erott@37872: (* cut and paste for math.tex erott@37872: *) erott@37872: erott@37872: (*2.2. *) erott@37872: "a + b * 3"; Walther@60566: TermC.parse_test @{context} "a + b * 3"; Walther@60566: val term = TermC.parse_test @{context} "a + b * 3"; erott@37872: atomt term; Walther@60650: TermC.atom_trace_detail @{context} term; erott@37872: erott@37872: (*2.3. Theories and parsing*) erott@37872: erott@37872: > Isac.thy; erott@37872: val it = erott@37872: {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp, erott@37872: Sum_Type, Relation, Record, Inductive, Transitive_Closure, erott@37872: Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power, erott@37872: SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe, erott@37872: Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv, erott@37872: IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map, erott@37872: Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd, erott@37872: RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow, erott@37872: Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix, erott@37872: Float, ComplexI, Descript, Atools, Simplify, Poly, Rational, PolyMinus, erott@37872: Equation, LinEq, Root, RootEq, RatEq, RootRat, RootRatEq, PolyEq, Vect, erott@37872: Calculus, Trig, LogExp, Diff, DiffApp, Integrate, EqSystem, Biegelinie, erott@37872: AlgEin, Test, Isac} : Theory.theory erott@37872: erott@37872: Group.thy erott@37872: suche nach '*' Link: http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/Groups.html erott@37872: locale semigroup = erott@37872: fixes f :: "'a => 'a => 'a" (infixl "*" 70) erott@37872: assumes assoc [ac_simps]: "a * b * c = a * (b * c)" erott@37872: erott@37872: > parse; erott@37872: val it = fn : Theory.theory -> string -> Thm.cterm Library.option erott@37872: erott@37872: erott@37872: erott@37872: > (*-1-*); erott@37872: > parse HOL.thy "2^^^3"; erott@37872: *** Inner lexical error at: "^^^3" erott@37872: val it = None : Thm.cterm Library.option erott@37872: > (*-2-*); erott@37872: > parse HOL.thy "d_d x (a + x)"; erott@37872: val it = None : Thm.cterm Library.option erott@37872: > (*-3-*); erott@37872: > parse Rational.thy "2^^^3"; erott@37872: val it = Some "2 ^^^ 3" : Thm.cterm Library.option erott@37872: > (*-4-*); erott@37872: val Some t4 = parse Rational.thy "d_d x (a + x)"; erott@37872: val t4 = "d_d x (a + x)" : Thm.cterm erott@37872: > (*-5-*); erott@37872: val Some t5 = parse Diff.thy "d_d x (a + x)"; erott@37872: val t5 = "d_d x (a + x)" : Thm.cterm erott@37872: erott@37872: erott@37872: > term_of; erott@37872: val it = fn : Thm.cterm -> Term.term erott@37872: > term_of t4; erott@37872: val it = erott@37872: Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ erott@37872: Free ("x", "RealDef.real") $ erott@37872: (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $ erott@37872: Free ("a", "RealDef.real") $ Free ("x", "RealDef.real")) erott@37872: : Term.term erott@37872: > term_of t5; erott@37872: val it = erott@37872: Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ erott@37872: Free ("x", "RealDef.real") $ erott@37872: (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $ erott@37872: Free ("a", "RealDef.real") $ Free ("x", "RealDef.real")) erott@37872: : Term.term erott@37872: erott@37872: > print_depth; erott@37872: val it = fn : int -> unit erott@37872: erott@37872: erott@37872: erott@37872: erott@37872: erott@37872: > (*-4-*) val thy = Rational.thy; erott@37872: val thy = erott@37872: {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp, erott@37872: Sum_Type, Relation, Record, Inductive, Transitive_Closure, erott@37872: Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power, erott@37872: SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe, erott@37872: Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv, erott@37872: IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map, erott@37872: Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd, erott@37872: RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow, erott@37872: Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix, erott@37872: Float, ComplexI, Descript, Atools, Simplify, Poly, Rational} erott@37872: : Theory.theory Walther@60650: > ((TermC.atom_trace_detail @{context}) o term_of o the o (parse thy)) "d_d x (a + x)"; erott@37872: erott@37872: *** erott@37872: *** Free (d_d, [real, real] => real) erott@37872: *** . Free (x, real) erott@37872: *** . Const (op +, [real, real] => real) erott@37872: *** . . Free (a, real) erott@37872: *** . . Free (x, real) erott@37872: *** erott@37872: erott@37872: val it = () : unit erott@37872: > (*-5-*) val thy = Diff.thy; erott@37872: val thy = erott@37872: {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp, erott@37872: Sum_Type, Relation, Record, Inductive, Transitive_Closure, erott@37872: Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power, erott@37872: SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe, erott@37872: Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv, erott@37872: IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map, erott@37872: Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd, erott@37872: RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow, erott@37872: Ring_and_Field, Complex_Numbers, Real, Calculus, Trig, ListG, Tools, erott@37872: Script, Typefix, Float, ComplexI, Descript, Atools, Simplify, Poly, erott@37872: Equation, LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq, erott@37872: PolyEq, LogExp, Diff} : Theory.theory erott@37872: Walther@60650: > ((TermC.atom_trace_detail @{context}) o term_of o the o (parse thy)) "d_d x (a + x)"; erott@37872: erott@37872: *** erott@37872: *** Const (Diff.d_d, [real, real] => real) erott@37872: *** . Free (x, real) erott@37872: *** . Const (op +, [real, real] => real) erott@37872: *** . . Free (a, real) erott@37872: *** . . Free (x, real) erott@37872: *** erott@37872: erott@37872: val it = () : unit erott@37872: erott@37872: erott@37872: erott@37872: > print_depth 1; erott@37872: val it = () : unit erott@37872: > term_of t4; erott@37872: val it = erott@37872: Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $ ... erott@37872: : Term.term erott@37872: erott@37872: erott@37872: > print_depth 1; erott@37872: val it = () : unit erott@37872: > term_of t5; erott@37872: val it = erott@37872: Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $ erott@37872: ... : Term.term erott@37872: erott@37872: erott@37872: erott@37872: -------------------------------------------ALT... erott@37872: explode it; erott@37872: \footnote{ erott@37872: print_depth 9; erott@37872: explode "a + b * 3"; erott@37872: } erott@37872: erott@37872: (*unschoen*) erott@37872: erott@37872: -------------------------------------------ALT... erott@37872: HOL.thy; erott@37872: parse; erott@37872: parse thy "a + b * 3"; erott@37872: val t = (term_of o the) it; erott@37872: term_of; erott@37872: erott@37872: (*2.3. Displaying terms*) erott@37872: print_depth; erott@37872: ////Compiler.Control.Print.printDepth; erott@37872: ? Compiler.Control.Print.printDepth:= 2; erott@37872: t; erott@37872: ?Compiler.Control.Print.printDepth:= 6; erott@37872: t; erott@37872: ?Compiler.Control.Print.printLength; erott@37872: ?Compiler.Control.Print.stringDepth; erott@37872: atomt; erott@37872: atomt t; Walther@60650: TermC.atom_trace_detail @{context}; Walther@60650: TermC.atom_trace_detail @{context} t; erott@37872: (*Give it a try: the mathematics knowledge grows*) erott@37872: parse HOL.thy "2^^^3"; erott@37872: parse HOL.thy "d_d x (a + x)"; erott@37872: ?parse RatArith.thy "#2^^^#3"; erott@37872: ?parse RatArith.thy "d_d x (a + x)"; erott@37872: parse Differentiate.thy "d_d x (a + x)"; erott@37872: ?parse Differentiate.thy "#2^^^#3"; erott@37872: (*don't trust the string representation*) erott@37872: ?val thy = RatArith.thy; Walther@60650: ((TermC.atom_trace_detail @{context} thy) o term_of o the o (parse thy)) "d_d x (a + x)"; erott@37872: ?val thy = Differentiate.thy; Walther@60650: ((TermC.atom_trace_detail @{context} thy) o term_of o the o (parse thy)) "d_d x (a + x)"; erott@37872: erott@37872: (*2.4. Converting terms*) erott@37872: term_of; erott@37872: the; erott@37872: val t = (term_of o the o (parse thy)) "a + b * 3"; erott@37872: erott@37872: sign_of; erott@37872: cterm_of; erott@37872: val ct = cterm_of (sign_of thy) t; erott@37872: erott@37872: Sign.string_of_term; erott@37872: Sign.string_of_term (sign_of thy) t; erott@37872: erott@37872: string_of_cterm; erott@37872: string_of_cterm ct; erott@37872: erott@37872: (*2.5. Theorems *) erott@37872: ?theorem' := overwritel (!theorem', erott@37872: [("diff_const",num_str diff_const) erott@37872: ]); erott@37872: erott@37872: (** 3. Rewriting **) erott@37872: (*3.1. The arguments for rewriting*) erott@37872: HOL.thy; erott@37872: "HOL.thy" : theory'; erott@37872: sqrt_right; Walther@60586: "sqrt_right" : rew_ord; erott@37872: eval_rls; erott@37872: "eval_rls" : rls'; erott@37872: diff_sum; erott@37872: ("diff_sum", "") : thm'; erott@37872: erott@37872: (*3.2. The functions for rewriting*) erott@37872: rewrite_; erott@37872: rewrite; erott@37872: erott@37872: > val thy' = "Diff.thy"; erott@37872: val thy' = "Diff.thy" : string erott@37872: > val ct = "d_d x (a * 3 + b)"; erott@37872: val ct = "d_d x (a * 3 + b)" : string erott@37872: > val thm = ("diff_sum",""); erott@37872: val thm = ("diff_sum", "") : string * string erott@37872: > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true erott@37872: [("bdv","x::real")] thm ct; erott@37872: val ct = "d_d x (a * 3) + d_d x b" : cterm' erott@37872: > val thm = ("diff_prod_const",""); erott@37872: val thm = ("diff_prod_const", "") : string * string erott@37872: > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true erott@37872: [("bdv","x::real")] thm ct; erott@37872: val ct = "a * d_d x 3 + d_d x b" : cterm' erott@37872: erott@37872: erott@37872: erott@37872: > val thy' = "Diff.thy"; erott@37872: val thy' = "Diff.thy" : string erott@37872: > val ct = "d_d x (a + a * (2 + b))"; erott@37872: val ct = "d_d x (a + a * (2 + b))" : string erott@37872: > val thm = ("diff_sum",""); erott@37872: val thm = ("diff_sum", "") : string * string erott@37872: > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true erott@37872: [("bdv","x::real")] thm ct; erott@37872: val ct = "d_d x a + d_d x (a * (2 + b))" : cterm' erott@37872: erott@37872: > val thm = ("diff_prod_const",""); erott@37872: val thm = ("diff_prod_const", "") : string * string erott@37872: > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true erott@37872: [("bdv","x::real")] thm ct; erott@37872: val ct = "d_d x a + a * d_d x (2 + b)" : cterm' erott@37872: erott@37872: erott@37872: erott@37872: (*Give it a try: rewriting*) erott@37872: val thy' = "Diff.thy"; erott@37872: val ct = "d_d x (x ^^^ 2 + 3 * x + 4)"; erott@37872: val thm = ("diff_sum",""); erott@37872: val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true [("bdv","x::real")] thm ct; erott@37872: val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true [("bdv","x::real")] thm ct; erott@37872: val thm = ("diff_prod_const",""); erott@37872: val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true [("bdv","x::real")] thm ct; erott@37872: (*Give it a try: conditional rewriting*) erott@37872: val thy' = "Isac.thy"; erott@37872: val ct' = "3 * a + 2 * (a + 1)"; erott@37872: val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n"); erott@37872: (*1*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; erott@37872: val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1"); erott@37872: ?(*2*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; erott@37872: ?val thm' = ("rcollect_right", erott@37872: "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n"); erott@37872: ?(*3*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; erott@37872: ?(*4*) val Some (ct',_) = calculate thy' "plus" ct'; erott@37872: ?(*5*) val Some (ct',_) = calculate thy' "times" ct'; erott@37872: erott@37872: (*Give it a try: functional programming*) erott@37872: val thy' = "InsSort.thy"; erott@37872: val ct = "sort [#1,#3,#2]" : cterm'; erott@37872: erott@37872: val thm = ("sort_def",""); erott@37872: ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); erott@37872: erott@37872: val thm = ("foldr_rec",""); erott@37872: ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); erott@37872: erott@37872: val thm = ("ins_base",""); erott@37872: ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); erott@37872: erott@37872: val thm = ("foldr_rec",""); erott@37872: ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); erott@37872: erott@37872: val thm = ("ins_rec",""); erott@37872: ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); erott@37872: erott@37872: ?val (ct,_) = the (calculate thy' "le" ct); erott@37872: erott@37872: val thm = ("if_True","(if True then ?x else ?y) = ?x"); erott@37872: ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); erott@37872: erott@37872: (*3.3. Variants of rewriting*) erott@37872: rewrite_inst_; erott@37872: rewrite_inst; erott@37872: erott@37872: rewrite_set_; erott@37872: rewrite_set; erott@37872: erott@37872: rewrite_set_inst_; erott@37872: rewrite_set_inst; erott@37872: erott@37872: toggle; erott@37872: toggle trace_rewrite; erott@37872: erott@37872: (*3.4. Rule sets*) erott@37872: sym; erott@37872: rearrange_assoc; erott@37872: erott@37872: (*Give it a try: remove parentheses*) erott@37872: ?val ct = (string_of_cterm o the o (parse RatArith.thy)) erott@37872: "a + (b * (c * d) + e)"; erott@37872: ?rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct; erott@37872: erott@37872: toggle trace_rewrite; erott@37872: ?rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct; erott@37872: erott@37872: (*3.5. Calculate numeric constants*) erott@37872: calculate; erott@37872: calculate_; erott@37872: erott@37872: ?calc_list; erott@37872: ?calculate "Isac.thy" "plus" "#1 + #2"; erott@37872: ?calculate "Isac.thy" "times" "#2 * #3"; erott@37872: ?calculate "Isac.thy" "power" "#2 ^^^ #3"; erott@37872: ?calculate "Isac.thy" "cancel_" "#9 // #12"; erott@37872: erott@37872: erott@37872: (** 4. Term orders **) erott@37872: (*4.1. Exmpales for term orders*) erott@37872: sqrt_right; erott@37872: tless_true; erott@37872: erott@37872: val t1 = (term_of o the o (parse thy)) "(sqrt a) + b"; erott@37872: val t2 = (term_of o the o (parse thy)) "b + (sqrt a)"; erott@37872: ?sqrt_right false SqRoot.thy (t1, t2); erott@37872: ?sqrt_right false SqRoot.thy (t2, t1); erott@37872: erott@37872: val t1 = (term_of o the o (parse thy)) "a + b*(sqrt c) + d"; erott@37872: val t2 = (term_of o the o (parse thy)) "a + (sqrt b)*c + d"; erott@37872: ?sqrt_right true SqRoot.thy (t1, t2); erott@37872: erott@37872: (*4.2. Ordered rewriting*) erott@37872: ac_plus_times; erott@37872: erott@37872: (*Give it a try: polynomial (normal) form*) erott@37872: val ct' = "#3 * a + b + #2 * a"; erott@37872: val thm' = ("radd_commute","") : thm'; erott@37872: ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; erott@37872: val thm' = ("rdistr_right_assoc_p","") : thm'; erott@37872: ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; erott@37872: ?val Some (ct',_) = calculate thy' "plus" ct'; erott@37872: erott@37872: val ct' = "3 * a + b + 2 * a" : cterm'; erott@37872: val thm' = ("radd_commute","") : thm'; erott@37872: ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; erott@37872: ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; erott@37872: ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; erott@37872: erott@37872: toggle trace_rewrite; erott@37872: ?rewrite_set "RatArith.thy" "eval_rls" false "ac_plus_times" ct; erott@37872: erott@37872: erott@37872: (** 5. The hierarchy of problem types **) erott@37872: (*5.1. The standard-function for 'matching'*) erott@37872: matches; erott@37872: erott@37872: val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1"; erott@37872: val p = (term_of o the o (parse thy)) "a * b^^^2 = c"; erott@37872: atomt p; Walther@60650: mk_Var; Walther@60650: val pat = mk_Var p; erott@37872: matches thy t pat; erott@37872: erott@37872: val t2 = (term_of o the o (parse thy)) "x^^^2 = 1"; erott@37872: matches thy t2 pat; erott@37872: erott@37872: val pat2 = (term_of o the o (parse thy)) "?u^^^2 = ?v"; erott@37872: matches thy t2 pat2; erott@37872: erott@37872: (*5.2. Accessing the hierarchy*) erott@37872: show_ptyps; erott@37872: show_ptyps(); erott@37872: get_pbt; erott@37872: ?get_pbt ["squareroot", "univariate", "equation"]; erott@37872: erott@37872: store_pbt; erott@37872: ?store_pbt erott@37872: (prep_pbt SqRoot.thy erott@37872: (["newtype","univariate","equation"], erott@37872: [("#Given" ,["equality e_","solveFor v_","errorBound err_"]), erott@37872: ("#Where" ,["contains_root (e_::bool)"]), erott@37872: ("#Find" ,["solutions v_i_"]) erott@37872: ], erott@37872: [("SqRoot.thy","square_equation")])); erott@37872: show_ptyps(); erott@37872: erott@37872: (*5.3. Internals of the datastructure*) erott@37872: (*5.4. Match a problem with a problem type*) erott@37872: ?val fmz = ["equality (#1 + #2 * x = #0)", erott@37872: "solveFor x", erott@37872: "solutions L"] : fmz; Walther@60769: by_formalise; Walther@60769: ?by_formalise fmz (get_pbt ["univariate","equation"]); Walther@60769: ?by_formalise fmz (get_pbt ["linear","univariate","equation"]); Walther@60769: ?by_formalise fmz (get_pbt ["squareroot","univariate","equation"]); erott@37872: erott@37872: (*5.5. Refine a problem specification *) erott@37872: refine; erott@37872: ?val fmz = ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))", erott@37872: "solveFor x","errorBound (eps=#0)", erott@37872: "solutions L"]; erott@37872: ?refine fmz ["univariate","equation"]; erott@37872: erott@37872: ?val fmz = ["equality (x+#1=#2)", erott@37872: "solveFor x","errorBound (eps=#0)", erott@37872: "solutions L"]; erott@37872: ?refine fmz ["univariate","equation"]; erott@37872: erott@37872: erott@37872: (* 6. Do a calculational proof *) erott@37872: ?val fmz = ["equality ((x+#1) * (x+#2) = x^^^#2+#8)","solveFor x", erott@37872: "errorBound (eps=#0)","solutions L"]; erott@37872: val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"], erott@37872: ("SqRoot.thy","no_met")); erott@37872: erott@37872: (*6.1. Initialize the calculation*) erott@37872: val p = e_pos'; val c = []; erott@37872: ?val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met))); erott@37872: ?val (p,_,f,nxt,_,pt) = me (mID,m) p c EmptyPtree; erott@37872: erott@37872: ?Compiler.Control.Print.printDepth:=8; erott@37872: ?f; erott@37872: ?Compiler.Control.Print.printDepth:=4; erott@37872: erott@37872: ?nxt; erott@37872: ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: erott@37872: (*6.2. The phase of modeling*) erott@37872: ?nxt; erott@37872: ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: erott@37872: ?Compiler.Control.Print.printDepth:=8; erott@37872: ?f; erott@37872: ?Compiler.Control.Print.printDepth:=4; erott@37872: erott@37872: (*6.3. The phase of specification*) erott@37872: ?nxt; erott@37872: ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: erott@37872: erott@37872: val nxt = ("Specify_Problem", erott@37872: Specify_Problem ["polynomial","univariate","equation"]); erott@37872: ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: erott@37872: val nxt = ("Specify_Problem", erott@37872: Specify_Problem ["linear","univariate","equation"]); erott@37872: ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: ?Compiler.Control.Print.printDepth:=8;f;Compiler.Control.Print.printDepth:=4; erott@37872: erott@37872: val nxt = ("Refine_Problem", erott@37872: Refine_Problem ["linear","univariate","equation"]); erott@37872: ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: ?Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4; erott@37872: erott@37872: val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]); erott@37872: ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: ?Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4; erott@37872: erott@37872: ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: erott@37872: (*6.4. The phase of solving*) erott@37872: nxt; erott@37872: ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: erott@37872: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: erott@37872: (*6.5. The final phase: check the postcondition*) erott@37872: ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: erott@37872: erott@37872: erott@37872: erott@37872: erott@37872: