sel_rules: generalize "fun assod" to Rewrite tac -- Rewrite_Set containing tac, stopped withou success.
1.1 --- a/src/sml/ME/rewtools.sml Wed Jan 02 10:06:00 2008 +0100
1.2 +++ b/src/sml/ME/rewtools.sml Wed Jan 02 14:42:04 2008 +0100
1.3 @@ -612,25 +612,14 @@
1.4 > thms_of_rls rls;
1.5 *)
1.6
1.7 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@#@#@#@#
1.8 -(*. check if an _atomic_ (Thm, Calc) rule is contained in a rule set
1.9 - (recursivley down in Rls_) .*)
1.10 -fun contains_rule rule (Rls {rules,...}) =
1.11 -
1.12 - if eq_rule thm rule then true
1.13 - else
1.14 - | contains_rule (cal as Calc _) rule = eq_rule thm rule
1.15 - case
1.16 -
1.17 -fun thm_of_rule Erule = []
1.18 - | thm_of_rule (thm as Thm _) = [thm]
1.19 - | thm_of_rule (Calc _) = []
1.20 - | thm_of_rule (Rls_ rls) = thms_of_rls rls
1.21 -and thms_of_rls Erls = []
1.22 - | thms_of_rls (Rls {rules,...}) = (flat o (map thm_of_rule)) rules
1.23 - | thms_of_rls (Seq {rules,...}) = (flat o (map thm_of_rule)) rules
1.24 - | thms_of_rls (Rrls _) = [];
1.25 -@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@#@#@#@#*)
1.26 +(*. check if a rule is contained in a rule-set (recursivley down in Rls_);
1.27 + this rule can even be a rule-set itself.*)
1.28 +fun contains_rule r rls =
1.29 + let fun find (r, Rls_ rls) = finds (get_rules rls)
1.30 + | find r12 = eq_rule r12
1.31 + and finds [] = false
1.32 + | finds (r1 :: rs) = if eq_rule (r, r1) then true else finds rs;
1.33 + in finds (get_rules rls) end;
1.34
1.35 (*. try if a rewrite-rule is applicable to a given formula;
1.36 in case of rule-sets (recursivley) collect all _atomic_ rewrites .*)
2.1 --- a/src/sml/ME/script.sml Wed Jan 02 10:06:00 2008 +0100
2.2 +++ b/src/sml/ME/script.sml Wed Jan 02 14:42:04 2008 +0100
2.3 @@ -618,36 +618,40 @@
2.4 8.01:
2.5 tac_ SubProblem with args completed from script
2.6 .*)
2.7 -fun assod pt d (m as Rewrite_Inst' (thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))
2.8 - (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $ b $ f_) =
2.9 - if thmID = thmID_ then
2.10 - if f = f_ then ((*writeln"3### assod ..Ass";*)Ass (m,f'))
2.11 - else ((*writeln"3### assod ..AssWeak";*)AssWeak(m, f'))
2.12 - else ((*writeln"3### assod ..NotAss";*)NotAss)
2.13 +fun assod pt d (m as Rewrite_Inst' (thy',rod,rls,put,subs,(thmID,thm),f,(f',asm))) stac =
2.14 + (case stac of
2.15 + (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $b$f_)=>
2.16 + if thmID = thmID_ then
2.17 + if f = f_ then ((*writeln"3### assod ..Ass";*)Ass (m,f'))
2.18 + else ((*writeln"3### assod ..AssWeak";*)AssWeak(m, f'))
2.19 + else ((*writeln"3### assod ..NotAss";*)NotAss)
2.20 + | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $_$f_)=>
2.21 + if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_) then
2.22 + if f = f_ then Ass (m,f') else AssWeak (m,f')
2.23 + else NotAss
2.24 + | _ => NotAss)
2.25
2.26 - | assod pt d (m as Rewrite' (thy,rod,rls,put,(thmID,thm),f,(f',asm)))
2.27 - (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) =
2.28 - ((*writeln("3### assod: stac = "^
2.29 - (Sign.string_of_term (sign_of (assoc_thy thy)) t));
2.30 - writeln("3### assod: f(m)= "^
2.31 - (Sign.string_of_term (sign_of (assoc_thy thy)) f));*)
2.32 - if thmID = thmID_ then
2.33 - if f = f_ then ((*writeln"3### assod ..Ass";*)Ass (m,f'))
2.34 - else ((*writeln"### assod ..AssWeak";
2.35 - writeln("### assod: f(m) = "^
2.36 - (Sign.string_of_term (sign_of (assoc_thy thy)) f));
2.37 - writeln("### assod: f(stac)= "^
2.38 - (Sign.string_of_term (sign_of (assoc_thy thy)) f_));*)
2.39 - AssWeak (m,f'))
2.40 - else ((*writeln"3### assod ..NotAss";*)NotAss))
2.41 -
2.42 -(*#@#@#@#@#@#@#@#@#@#@#@#@#@#@#@#@#@#@#
2.43 - | assod pt d (m as Rewrite' (thy,rod,rls,put,(thmID,thm),f,(f',asm)))
2.44 - (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =
2.45 - if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls) then
2.46 - if f = f_ then Ass (m,f') else AssWeak (m,f')
2.47 - else NotAss
2.48 -#@#@#@#@#@#@#@#@#@#@#@#@#@#@#@#@#@#@#*)
2.49 + | assod pt d (m as Rewrite' (thy,rod,rls,put,(thmID,thm),f,(f',asm))) stac =
2.50 + (case stac of
2.51 + (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) =>
2.52 + ((*writeln("3### assod: stac = "^
2.53 + (Sign.string_of_term (sign_of (assoc_thy thy)) t));
2.54 + writeln("3### assod: f(m)= "^
2.55 + (Sign.string_of_term (sign_of (assoc_thy thy)) f));*)
2.56 + if thmID = thmID_ then
2.57 + if f = f_ then ((*writeln"3### assod ..Ass";*)Ass (m,f'))
2.58 + else ((*writeln"### assod ..AssWeak";
2.59 + writeln("### assod: f(m) = "^
2.60 + (Sign.string_of_term (sign_of(assoc_thy thy)) f));
2.61 + writeln("### assod: f(stac)= "^
2.62 + (Sign.string_of_term(sign_of(assoc_thy thy))f_))*)
2.63 + AssWeak (m,f'))
2.64 + else ((*writeln"3### assod ..NotAss";*)NotAss))
2.65 + | (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =>
2.66 + if contains_rule (Thm (thmID, refl(*dummy*))) rls then
2.67 + if f = f_ then Ass (m,f') else AssWeak (m,f')
2.68 + else NotAss
2.69 + | _ => NotAss)
2.70
2.71 (*val f = (term_of o the o (parse thy))"#0+(sqrt(sqrt(sqrt a))^^^#2)^^^#2=#0";
2.72 > val f'= (term_of o the o (parse thy))"#0+(sqrt(sqrt a))^^^#2=#0";
2.73 @@ -684,11 +688,23 @@
2.74 if f = f_ then Ass (m,f') else AssWeak (m,f')
2.75 else NotAss
2.76
2.77 - | assod pt d (m as Calculate' (thy',op_,f,(f',thm')))
2.78 - (Const ("Script.Calculate",_) $ Free (op__,_) $ f_) =
2.79 - if op_ = op__ then
2.80 - if f = f_ then Ass (m,f') else AssWeak (m,f')
2.81 - else NotAss
2.82 + | assod pt d (m as Calculate' (thy',op_,f,(f',thm'))) stac =
2.83 + (case stac of
2.84 + (Const ("Script.Calculate",_) $ Free (op__,_) $ f_) =>
2.85 + if op_ = op__ then
2.86 + if f = f_ then Ass (m,f') else AssWeak (m,f')
2.87 + else NotAss
2.88 + | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free(rls_,_) $_$f_)=>
2.89 + if contains_rule (Calc (snd (assoc1 (!calclist', op_))))
2.90 + (assoc_rls rls_) then
2.91 + if f = f_ then Ass (m,f') else AssWeak (m,f')
2.92 + else NotAss
2.93 + | (Const ("Script.Rewrite'_Set",_) $ Free (rls_, _) $ _ $ f_) =>
2.94 + if contains_rule (Calc (snd (assoc1 (!calclist', op_))))
2.95 + (assoc_rls rls_) then
2.96 + if f = f_ then Ass (m,f') else AssWeak (m,f')
2.97 + else NotAss
2.98 + | _ => NotAss)
2.99
2.100 | assod pt _ (m as Check_elementwise' (consts,_,(consts_chkd,_)))
2.101 (Const ("Script.Check'_elementwise",_) $ consts' $ _) =
3.1 --- a/src/smltest/IsacKnowledge/eqsystem.sml Wed Jan 02 10:06:00 2008 +0100
3.2 +++ b/src/smltest/IsacKnowledge/eqsystem.sml Wed Jan 02 14:42:04 2008 +0100
3.3 @@ -1108,6 +1108,7 @@
3.4 "[c = (-1 * (L * q_0) + 0) / -1,\n L * c + c_2 = -1 * (-1 * q_0 * L ^^^ 2 / 2) + 0, c_4 = 0, c_3 = 0]";
3.5 val Some (t,_) =
3.6 rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
3.7 +
3.8 term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_4 = 0, c_3 = 0]";
3.9 val Some (t,_) = rewrite_set_ thy false order_system t;
3.10 if term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]" then ()
3.11 @@ -1132,20 +1133,25 @@
3.12 case nxt of (_,Apply_Method ["EqSystem", "normalize", "4x4"]) => ()
3.13 | _ => raise error "eqsystem.sml [EqSystem,normalize,4x4] specify";
3.14 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.15 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.16 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.17 +"bbbbbbbbbbbbbbbbbbbbbbbbbbbbb outcommented vvvvvvvvvvvvvvvvvvvvvv";
3.18 +(*vvvWN080102 Exception- Match raised
3.19 + since assod Rewrite .. Rewrite'_Set
3.20 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.21
3.22 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.23 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.24 +
3.25 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.26 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.27 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.28 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.29 if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]"
3.30 then () else raise error "eqsystem.sml: exp 7.70 normalize 4x4 by met changed";
3.31 +--------------------------------------------------------------------------*)
3.32
3.33 "----- 7.70 with met top_down_: ";
3.34 "--- scr [EqSystem,top_down_substitution,4x4] -- a saved trial";
3.35 -(*---vvv-this script failed with if ?!?-------------------------------------*)
3.36 +(*---vvv-this script failed with if ?!?-------------------------------------*)
3.37 val str =
3.38 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
3.39 \ (let e1_ = hd es_; \
3.40 @@ -1386,7 +1392,7 @@
3.41 "----------- 4x4 systems from Biegelinie -------------------------";
3.42 "----------- 4x4 systems from Biegelinie -------------------------";
3.43 "----------- 4x4 systems from Biegelinie -------------------------";
3.44 -(*GOON replace this test with 7.70 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@2*)
3.45 +(*GOON replace this test with 7.70 *)
3.46 "----- Bsp 7.27";
3.47 val fmz = ["equalities \
3.48 \[0 = c_4, \
3.49 @@ -1409,6 +1415,8 @@
3.50 \ 0 = c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
3.51 \ 0 = c_2, \
3.52 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]";
3.53 +(*vvvWN080102 Exception- Match raised
3.54 + since assod Rewrite .. Rewrite'_Set
3.55 "------------------------------------------- simplify_System_parenthesized...";
3.56 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.57 "[0 = c_4, \
3.58 @@ -1427,7 +1435,7 @@
3.59 \ c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2) + -1 * (L * c)]";
3.60 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.61
3.62 -
3.63 +---------------------------------------------------------------------*)
3.64
3.65 (*
3.66 use"../smltest/IsacKnowledge/eqsystem.sml";
4.1 --- a/src/smltest/IsacKnowledge/polyminus.sml Wed Jan 02 10:06:00 2008 +0100
4.2 +++ b/src/smltest/IsacKnowledge/polyminus.sml Wed Jan 02 14:42:04 2008 +0100
4.3 @@ -20,6 +20,7 @@
4.4 "----------- met probe fuer_polynom ------------------------------";
4.5 "----------- pbl polynom probe -----------------------------------";
4.6 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
4.7 +"----------- try fun applyTactics --------------------------------";
4.8 "-----------------------------------------------------------------";
4.9 "-----------------------------------------------------------------";
4.10 "-----------------------------------------------------------------";
4.11 @@ -264,6 +265,31 @@
4.12 show_pt pt;
4.13
4.14
4.15 +"----------- try fun applyTactics --------------------------------";
4.16 +"----------- try fun applyTactics --------------------------------";
4.17 +"----------- try fun applyTactics --------------------------------";
4.18 +states:=[];
4.19 +CalcTree [(["term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
4.20 + "normalform N"],
4.21 + ("PolyMinus.thy",["polynom","vereinfachen"],
4.22 + ["simplification","for_polynomials","with_minus"]))];
4.23 +moveActiveRoot 1;
4.24 +autoCalculate 1 CompleteCalcHead;
4.25 +autoCalculate 1 (Step 1);
4.26 +autoCalculate 1 (Step 1);
4.27 +
4.28 +val ((pt,p),_) = get_calc 1;
4.29 +show_pt pt;
4.30 +fetchApplicableTactics 1 0 p;
4.31 +val appltacs = sel_appl_atomic_tacs pt p;
4.32 +
4.33 +(*vvv this gives <CALCMESSAGE> failure </CALCMESSAGE>*)
4.34 +applyTactic 1 p (hd appltacs);
4.35 +applyTactic 1 p ((hd o tl) appltacs);
4.36 +
4.37 +(*vvv only this (= autoCalculate tac) works*)
4.38 +applyTactic 1 p (Rewrite_Set "fasse_zusammen");
4.39 +
4.40 (*
4.41 use"../smltest/IsacKnowledge/polyminus.sml";
4.42 use"polyminus.sml";
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/smltest/ME/me.sml Wed Jan 02 14:42:04 2008 +0100
5.3 @@ -0,0 +1,528 @@
5.4 +(* tests on me.sml
5.5 + author: Walther Neuper
5.6 + 060225,
5.7 + (c) due to copyright terms
5.8 +
5.9 +use"../smltest/ME/me.sml";
5.10 +use"me.sml";
5.11 +*)
5.12 +
5.13 +"-----------------------------------------------------------------";
5.14 +"table of contents -----------------------------------------------";
5.15 +"-----------------------------------------------------------------";
5.16 +"=====new ptree 1: crippled by cut_level_'_ ======================";
5.17 +"-------------- get_interval from ctree with move_dn:modspec.sml -";
5.18 +"=====new ptree 2 without changes ================================";
5.19 +"-------------- getFormulaeFromTo --------------------------------";
5.20 +"autoCalculate";
5.21 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
5.22 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
5.23 +"--------- maximum-example: complete_metitms ---------------------";
5.24 +"--------- maximum-example: complete_mod -------------------------";
5.25 +"-----------------------------------------------------------------";
5.26 +"-----------------------------------------------------------------";
5.27 +"-----------------------------------------------------------------";
5.28 +
5.29 +
5.30 +
5.31 +"=====new ptree 1: crippled by cut_level_'_ ======================";
5.32 +"=====new ptree 1: crippled by cut_level_'_ ======================";
5.33 +"=====new ptree 1: crippled by cut_level_'_ ======================";
5.34 +states:=[];
5.35 +CalcTree
5.36 +[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
5.37 + "solveFor x","solutions L"],
5.38 + ("RatEq.thy",["univariate","equation"],["no_met"]))];
5.39 +Iterator 1; moveActiveRoot 1;
5.40 +autoCalculate 1 CompleteCalc;
5.41 +
5.42 +getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*)
5.43 +getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*)
5.44 +getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*)
5.45 +getTactic 1 ([4,1],Res);(*Rewrite all_left*)
5.46 +getTactic 1 ([4,2],Res);(*Rewrite_Set expand_binoms*)
5.47 +getTactic 1 ([4,3],Res);(*Rewrite_Set_Inst make_ratpoly_in*)
5.48 +
5.49 +moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
5.50 +moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*);
5.51 +moveActiveFormula 1 ([3],Res)(*3.1.*);
5.52 +moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
5.53 +moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Script Stepwise t_=*);
5.54 +
5.55 +moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
5.56 +interSteps 1 ([1],Res)(*..is activeFormula !?!*);
5.57 +
5.58 +getTactic 1 ([1,1],Res);(*Rewrite real_diff_minus*)
5.59 +getTactic 1 ([1,2],Res);(*Rewrite real_diff_minus*)
5.60 +getTactic 1 ([1,3],Res);(*Rewrite real_diff_minus*)
5.61 +getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*)
5.62 +
5.63 +moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
5.64 +interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
5.65 +val ((pt,_),_) = get_calc 1;
5.66 +writeln(pr_ptree pr_short pt);
5.67 +(*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
5.68 + ###########################################################################*)
5.69 +val (pt, _) = cut_level_'_ [] [] pt ([4,1],Frm); (*#*)
5.70 +(*##########################################################################*)
5.71 +writeln(pr_ptree pr_short pt);
5.72 +(*##########################################################################
5.73 + attention: the ctree in states is still the old (perfect) !!!
5.74 +############################################################################*)
5.75 +
5.76 +
5.77 +
5.78 +"-------------- get_interval from ctree with move_dn:modspec.sml -";
5.79 +"-------------- get_interval from ctree with move_dn:modspec.sml -";
5.80 +"-------------- get_interval from ctree with move_dn:modspec.sml -";
5.81 +writeln(pr_ptree pr_short pt);
5.82 +writeln(posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
5.83 +
5.84 +case map fst (get_interval ([],Frm) ([],Res) 99999 pt) of
5.85 + [([], Frm),
5.86 + ([1], Frm),
5.87 + ([1, 1], Frm),
5.88 + ([1, 1], Res),
5.89 + ([1, 2], Res),
5.90 + ([1, 3], Res),
5.91 + ([1, 4], Res),
5.92 + ([1], Res),
5.93 + ([2], Res),
5.94 + ([3], Res),
5.95 + ([4], Pbl),
5.96 + ([4, 1], Frm),
5.97 + ([4, 1, 1], Frm),
5.98 + ([4, 1, 1], Res),
5.99 + ([4, 1], Res),
5.100 + ([4, 2], Res),
5.101 + ([4, 3], Pbl),
5.102 + ([4, 3, 1], Frm),
5.103 + ([4, 3, 1], Res),
5.104 + ([4, 3, 2], Res),
5.105 + ([4, 3, 3], Res),
5.106 + ([4, 3, 4], Res),
5.107 + ([4, 3, 5], Res),
5.108 + ([4, 3], Res),
5.109 + ([4], Res),
5.110 + ([5], Res),
5.111 + ([], Res)] => ()
5.112 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f";
5.113 +case map fst (get_interval ([],Frm) ([],Res) 1 pt) of
5.114 + [([], Frm),
5.115 + ([1], Frm),
5.116 + ([1], Res),
5.117 + ([2], Res),
5.118 + ([3], Res),
5.119 + ([4], Pbl),
5.120 + ([4], Res),
5.121 + ([5], Res),
5.122 + ([], Res)] => ()
5.123 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f";
5.124 +case map fst (get_interval ([],Frm) ([],Res) 0 pt) of
5.125 + [([], Frm),
5.126 + ([], Res)] => ()
5.127 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f";
5.128 +
5.129 +case map fst (get_interval ([1,3],Res) ([4,1,1],Frm) 99999 pt) of
5.130 + [([1, 3], Res),
5.131 + ([1, 4], Res),
5.132 + ([1], Res),
5.133 + ([2], Res),
5.134 + ([3], Res),
5.135 + ([4], Pbl),
5.136 + ([4, 1], Frm),
5.137 + ([4, 1, 1], Frm)] => ()
5.138 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1a";
5.139 +
5.140 +(*this pos' is not generated bu move_dn:......vvv: goes to end of calc*)
5.141 +case map fst (get_interval ([2],Res) ([4,3,2],Frm) 99999 pt) of
5.142 + [([2], Res),
5.143 + ([3], Res),
5.144 + ([4], Pbl),
5.145 + ([4, 1], Frm),
5.146 + ([4, 1, 1], Frm),
5.147 + ([4, 1, 1], Res),
5.148 + ([4, 1], Res),
5.149 + ([4, 2], Res),
5.150 + ([4, 3], Pbl),
5.151 + ([4, 3, 1], Frm),
5.152 + ([4, 3, 1], Res),
5.153 + ([4, 3, 2], Res),
5.154 + ([4, 3, 3], Res),(*this is beyond 'to'*)
5.155 + ([4, 3, 4], Res),(*this is beyond 'to'*)
5.156 + ([4, 3, 5], Res),(*this is beyond 'to'*)
5.157 + ([4, 3], Res), (*this is beyond 'to'*)
5.158 + ([4], Res), (*this is beyond 'to'*)
5.159 + ([5], Res), (*this is beyond 'to'*)
5.160 + ([], Res)] => () (*this is beyond 'to'*)
5.161 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1b";
5.162 +case map fst (get_interval ([1,4],Res) ([4,3,1],Frm) 99999 pt) of
5.163 + [([1, 4], Res),
5.164 + ([1], Res),
5.165 + ([2], Res),
5.166 + ([3], Res),
5.167 + ([4], Pbl),
5.168 + ([4, 1], Frm),
5.169 + ([4, 1, 1], Frm),
5.170 + ([4, 1, 1], Res),
5.171 + ([4, 1], Res),
5.172 + ([4, 2], Res),
5.173 + ([4, 3], Pbl),
5.174 + ([4, 3, 1], Frm)] => ()
5.175 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1c";
5.176 +case map fst (get_interval ([4,2],Res) ([5],Res) 99999 pt) of
5.177 + [([4, 2], Res),
5.178 + ([4, 3], Pbl),
5.179 + ([4, 3, 1], Frm),
5.180 + ([4, 3, 1], Res),
5.181 + ([4, 3, 2], Res),
5.182 + ([4, 3, 3], Res),
5.183 + ([4, 3, 4], Res),
5.184 + ([4, 3, 5], Res),
5.185 + ([4, 3], Res),
5.186 + ([4], Res),
5.187 + ([5], Res)]=>()
5.188 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1d";
5.189 +case map fst (get_interval ([],Frm) ([4,3,2],Res) 99999 pt) of
5.190 + [([], Frm),
5.191 + ([1], Frm),
5.192 + ([1, 1], Frm),
5.193 + ([1, 1], Res),
5.194 + ([1, 2], Res),
5.195 + ([1, 3], Res),
5.196 + ([1, 4], Res),
5.197 + ([1], Res),
5.198 + ([2], Res),
5.199 + ([3], Res),
5.200 + ([4], Pbl),
5.201 + ([4, 1], Frm),
5.202 + ([4, 1, 1], Frm),
5.203 + ([4, 1, 1], Res),
5.204 + ([4, 1], Res),
5.205 + ([4, 2], Res),
5.206 + ([4, 3], Pbl),
5.207 + ([4, 3, 1], Frm),
5.208 + ([4, 3, 1], Res),
5.209 + ([4, 3, 2], Res)] => ()
5.210 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1e";
5.211 +case map fst (get_interval ([4,3],Frm) ([4,3],Res) 99999 pt) of
5.212 + [([4, 3], Frm),
5.213 + ([4, 3, 1], Frm),
5.214 + ([4, 3, 1], Res),
5.215 + ([4, 3, 2], Res),
5.216 + ([4, 3, 3], Res),
5.217 + ([4, 3, 4], Res),
5.218 + ([4, 3, 5], Res),
5.219 + ([4, 3], Res)] => ()
5.220 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1g";
5.221 +
5.222 +
5.223 +
5.224 +
5.225 +"=====new ptree 2 without changes ================================";
5.226 +"=====new ptree 2 without changes ================================";
5.227 +"=====new ptree 2 without changes ================================";
5.228 +states:=[];
5.229 +CalcTree
5.230 +[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
5.231 + "solveFor x","solutions L"],
5.232 + ("RatEq.thy",["univariate","equation"],["no_met"]))];
5.233 +Iterator 1; moveActiveRoot 1;
5.234 +autoCalculate 1 CompleteCalc;
5.235 +val ((pt,_),_) = get_calc 1;
5.236 +writeln(pr_ptree pr_short pt);
5.237 +
5.238 +
5.239 +"-------------- getFormulaeFromTo --------------------------------";
5.240 +"-------------- getFormulaeFromTo --------------------------------";
5.241 +"-------------- getFormulaeFromTo --------------------------------";
5.242 +getFormulaeFromTo 1 ([4, 2], Res) ([4, 4], Pbl) 000;
5.243 +(*
5.244 +"@@@@@begin@@@@@" //...................................................
5.245 ++ " 1" //..............................................................
5.246 ++ "<GETELEMENTSFROMTO>" //...................................................
5.247 ++ " <CALCID> 1 </CALCID>" //..........................................
5.248 ++ " <POSFORMHEADS>" //................................................
5.249 ++ " <POSFORM>" //...................................................
5.250 ++ " <GENERATED>" //...............................................
5.251 ++ " <INTLIST>" //...............................................
5.252 ++ " <INT> 4 </INT>" //........................................
5.253 ++ " <INT> 3 </INT>" //........................................
5.254 ++ " </INTLIST>" //..............................................
5.255 ++ " <POS> Res </POS>" //........................................
5.256 ++ " </GENERATED>" //..............................................
5.257 ++ " <FORMULA>" //.................................................
5.258 ++ " <MATHML>" //................................................
5.259 ++ " <ISA> -6 * x + 5 * x ^^^ 2 = 0 </ISA>" //.................
5.260 ++ " </MATHML>" //...............................................
5.261 ++ " </FORMULA>" //................................................
5.262 ++ " </POSFORM>" //..................................................
5.263 ++ " <POSHEAD>" //...................................................
5.264 ++ " <GENERATED>" //...............................................
5.265 ++ " <INTLIST>" //...............................................
5.266 ++ " <INT> 4 </INT>" //........................................
5.267 ++ " <INT> 4 </INT>" //........................................
5.268 ++ " </INTLIST>" //..............................................
5.269 ++ " <POS> Pbl </POS>" //........................................
5.270 ++ " </GENERATED>" //..............................................
5.271 ++ " <CALCHEAD status = "correct">" //.............................
5.272 ++ " <HEAD>" //...................................................
5.273 ++ " <MATHML>" //...............................................
5.274 ++ " <ISA> solve (-6 * x + 5 * x ^^^ 2 = 0, x) </ISA>" //.....
5.275 ++ " </MATHML>" //..............................................
5.276 ++ " </HEAD>" //..................................................
5.277 ++ " <MODEL>" //.................................................
5.278 ++ " <GIVEN>" //...............................................
5.279 ++ " <ITEM status="correct">" //.............................
5.280 ++ " <MATHML>" //..........................................
5.281 ++ " <ISA> equality (-6 * x + 5 * x ^^^ 2 = 0) </ISA>" //
5.282 ++ " </MATHML>" //.........................................
5.283 ++ " </ITEM>" //.............................................
5.284 ++ " <ITEM status="correct">" //.............................
5.285 ++ " <MATHML>" //..........................................
5.286 ++ " <ISA> solveFor x </ISA>" //.........................
5.287 ++ " </MATHML>" //.........................................
5.288 ++ " </ITEM>" //.............................................
5.289 ++ " </GIVEN>" //..............................................
5.290 ++ " <WHERE>" //...............................................
5.291 ++ " <ITEM status="correct">" //.............................
5.292 ++ " <MATHML>" //..........................................
5.293 ++ " <ISA> matches (?a * ?v_ + ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"
5.294 ++ "matches (?v_ + ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" //......
5.295 ++ "matches (?v_ + ?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"
5.296 ++ "matches (?a * ?v_ + ?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"
5.297 ++ "matches (?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" //............
5.298 ++ "matches (?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) </ISA>" //..
5.299 ++ " </MATHML>" //.........................................
5.300 ++ " </ITEM>" //.............................................
5.301 ++ " </WHERE>" //..............................................
5.302 ++ " <FIND>" //................................................
5.303 ++ " <ITEM status="correct">" //.............................
5.304 ++ " <MATHML>" //..........................................
5.305 ++ " <ISA> solutions x_i </ISA>" //......................
5.306 ++ " </MATHML>" //.........................................
5.307 ++ " </ITEM>" //.............................................
5.308 ++ " </FIND>" //...............................................
5.309 ++ " <RELATE> </RELATE>" //...................................
5.310 ++ " </MODEL>" //................................................
5.311 ++ " <BELONGSTO> Pbl </BELONGSTO>" //............................
5.312 ++ " <SPECIFICATION>" //.........................................
5.313 ++ " <THEORYID> PolyEq.thy </THEORYID>" //.....................
5.314 ++ " <PROBLEMID>" //...........................................
5.315 ++ " <STRINGLIST>" //........................................
5.316 ++ " <STRING> bdv_only </STRING>" //.......................
5.317 ++ " <STRING> degree_2 </STRING>" //.......................
5.318 ++ " <STRING> polynomial </STRING>" //.....................
5.319 ++ " <STRING> univariate </STRING>" //.....................
5.320 ++ " <STRING> equation </STRING>" //.......................
5.321 ++ " </STRINGLIST>" //.......................................
5.322 ++ " </PROBLEMID>" //..........................................
5.323 ++ " <METHODID>" //............................................
5.324 ++ " <STRINGLIST>" //........................................
5.325 ++ " <STRING> PolyEq </STRING>" //.........................
5.326 ++ " <STRING> solve_d2_polyeq_bdvonly_equation </STRING>"
5.327 ++ " </STRINGLIST>" //.......................................
5.328 ++ " </METHODID>" //...........................................
5.329 ++ " </SPECIFICATION>" //........................................
5.330 ++ " </CALCHEAD>" //...............................................
5.331 ++ " </POSHEAD>" //..................................................
5.332 ++ " <POSFORMHEADS>" //................................................
5.333 ++ "</GETELEMENTSFROMTO>" //..................................................
5.334 ++ "@@@@@end@@@@@"
5.335 +*)
5.336 +
5.337 +
5.338 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
5.339 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
5.340 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
5.341 + val c = [];
5.342 + val (p,_,f,nxt,_,pt) = CalcTreeTEST
5.343 + [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
5.344 + ("Test.thy",
5.345 + ["linear","univariate","equation","test"],
5.346 + ["Test","solve_linear"]))];
5.347 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.348 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.349 + (*xt = Add_Given "solveFor x"*)
5.350 + writeln (itms2str thy (get_obj g_pbl pt (fst p)));
5.351 +(*[
5.352 +(0 ,[] ,false ,#Given ,Inc solveFor ,(??.empty, [])),
5.353 +(0 ,[] ,false ,#Find ,Inc solutions [] ,(??.empty, [])),
5.354 +(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0]))]*)
5.355 + val (pt,p) = complete_mod (pt, p);
5.356 + if itms2str thy (get_obj g_pbl pt (fst p)) = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]" then ()
5.357 + else raise error "completetest.sml: new behav. in complete_mod 1";
5.358 + writeln (itms2str thy (get_obj g_pbl pt (fst p)));
5.359 +(*[
5.360 +(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
5.361 +(2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
5.362 +(3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)
5.363 + val mits = get_obj g_met pt (fst p);
5.364 + if itms2str thy mits = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]"
5.365 + then () else raise error "completetest.sml: new behav. in complete_mod 2";
5.366 + writeln (itms2str thy mits);
5.367 +(*[
5.368 +(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
5.369 +(2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
5.370 +(3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)
5.371 +
5.372 +
5.373 +
5.374 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
5.375 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
5.376 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
5.377 + states:=[];
5.378 + CalcTree (*start of calculation, return No.1*)
5.379 + [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
5.380 + ("Test.thy",
5.381 + ["linear","univariate","equation","test"],
5.382 + ["Test","solve_linear"]))];
5.383 + Iterator 1; moveActiveRoot 1;
5.384 +
5.385 +(*
5.386 + autoCalculate 1 CompleteCalcHead;
5.387 + autoCalculate 1 (Step 1);
5.388 + refFormula 1 (get_pos 1 1);
5.389 +
5.390 +... works
5.391 +
5.392 + autoCalculate 1 CompleteCalcHead;
5.393 + fetchProposedTactic 1; (*-> Apply_Method*);
5.394 + setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
5.395 + autoCalculate 1 (Step 1);
5.396 + refFormula 1 (get_pos 1 1);
5.397 +
5.398 +... works *)
5.399 +
5.400 + autoCalculate 1 (Step 1);
5.401 + refFormula 1 (get_pos 1 1);
5.402 +
5.403 + autoCalculate 1 CompleteModel;
5.404 + refFormula 1 (get_pos 1 1);
5.405 +
5.406 + autoCalculate 1 CompleteCalcHead;
5.407 +(* *** complete_mod: only impl.for Pbl, called with ([], Met) FIXXXXXXXXXXME*)
5.408 +
5.409 +
5.410 +
5.411 +"--------- maximum-example: complete_metitms ---------------------";
5.412 +"--------- maximum-example: complete_metitms ---------------------";
5.413 +"--------- maximum-example: complete_metitms ---------------------";
5.414 + val (p,_,f,nxt,_,pt) =
5.415 + CalcTreeTEST
5.416 + [(["fixedValues [r=Arbfix]","maximum A",
5.417 + "valuesFor [a,b]",
5.418 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
5.419 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
5.420 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
5.421 +
5.422 + "boundVariable a","boundVariable b","boundVariable alpha",
5.423 + "interval {x::real. 0 <= x & x <= 2*r}",
5.424 + "interval {x::real. 0 <= x & x <= 2*r}",
5.425 + "interval {x::real. 0 <= x & x <= pi}",
5.426 + "errorBound (eps=(0::real))"],
5.427 + ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"])
5.428 + )];
5.429 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.430 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.431 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.432 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.433 + val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;
5.434 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.435 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.436 + (*nxt = Specify_Theory "DiffApp.thy"*)
5.437 + val (oris, _, _) = get_obj g_origin pt (fst p);
5.438 + writeln (oris2str oris);
5.439 +(*[
5.440 +(1, ["1","2","3"], #Given,fixedValues, ["[r = Arbfix]"]),
5.441 +(2, ["1","2","3"], #Find,maximum, ["A"]),
5.442 +(3, ["1","2","3"], #Find,valuesFor, ["[a]","[b]"]),
5.443 +(4, ["1","2"], #Relate,relations, ["[A = a * b]","[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"]),
5.444 +(5, ["3"], #Relate,relations, ["[A = a * b]","[a / 2 = r * sin alpha]","[b / 2 = r * cos alpha]"]),
5.445 +(6, ["1"], #undef,boundVariable, ["a"]),
5.446 +(7, ["2"], #undef,boundVariable, ["b"]),
5.447 +(8, ["3"], #undef,boundVariable, ["alpha"]),
5.448 +(9, ["1","2"], #undef,interval, ["{x. 0 <= x & x <= 2 * r}"]),
5.449 +(10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]),
5.450 +(11, ["1","2","3"], #undef,errorBound, ["eps = 0"])]*)
5.451 + val pits = get_obj g_pbl pt (fst p);
5.452 + writeln (itms2str thy pits);
5.453 +(*[
5.454 +(1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])),
5.455 +(2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])),
5.456 +(3 ,[1,2,3] ,true,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
5.457 +(4 ,[1,2] ,true,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
5.458 +2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
5.459 + val mits = get_obj g_met pt (fst p);
5.460 + val mits = complete_metitms oris pits []
5.461 + ((#ppc o get_met) ["DiffApp","max_by_calculus"]);
5.462 + writeln (itms2str thy mits);
5.463 +(*[
5.464 +(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
5.465 +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
5.466 +(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
5.467 +(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
5.468 +2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
5.469 +(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
5.470 +(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
5.471 +0 <= x & x <= 2 * r}])),
5.472 +(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
5.473 + if itms2str thy mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then ()
5.474 + else raise error "completetest.sml: new behav. in complete_metitms 1";
5.475 +
5.476 +
5.477 +"--------- maximum-example: complete_mod -------------------------";
5.478 +"--------- maximum-example: complete_mod -------------------------";
5.479 +"--------- maximum-example: complete_mod -------------------------";
5.480 + val (p,_,f,nxt,_,pt) =
5.481 + CalcTreeTEST
5.482 + [(["fixedValues [r=Arbfix]","maximum A",
5.483 + "valuesFor [a,b]",
5.484 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
5.485 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
5.486 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
5.487 +
5.488 + "boundVariable a","boundVariable b","boundVariable alpha",
5.489 + "interval {x::real. 0 <= x & x <= 2*r}",
5.490 + "interval {x::real. 0 <= x & x <= 2*r}",
5.491 + "interval {x::real. 0 <= x & x <= pi}",
5.492 + "errorBound (eps=(0::real))"],
5.493 + ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"])
5.494 + )];
5.495 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.496 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.497 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.498 + (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)
5.499 + val pits = get_obj g_pbl pt (fst p);
5.500 + writeln (itms2str thy pits);
5.501 +(*[
5.502 +(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
5.503 +(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),
5.504 +(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
5.505 +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)
5.506 + val (pt,p) = complete_mod (pt,p);
5.507 + val pits = get_obj g_pbl pt (fst p);
5.508 + if itms2str thy pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]"
5.509 + then () else raise error "completetest.sml: new behav. in complete_mod 3";
5.510 + writeln (itms2str thy pits);
5.511 +(*[
5.512 +(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
5.513 +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
5.514 +(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
5.515 +(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
5.516 +2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
5.517 + val mits = get_obj g_met pt (fst p);
5.518 + if itms2str thy mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]"
5.519 + then () else raise error "completetest.sml: new behav. in complete_mod 3";
5.520 + writeln (itms2str thy mits);
5.521 +(*[
5.522 +(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
5.523 +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
5.524 +(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
5.525 +(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
5.526 +2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
5.527 +(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
5.528 +(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
5.529 +0 <= x & x <= 2 * r}])),
5.530 +(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
5.531 +
6.1 --- a/src/smltest/ME/rewtools.sml Wed Jan 02 10:06:00 2008 +0100
6.2 +++ b/src/smltest/ME/rewtools.sml Wed Jan 02 14:42:04 2008 +0100
6.3 @@ -26,6 +26,7 @@
6.4 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
6.5 "-----------------------------------------------------------------";
6.6 "----------- fun filter_appl_rews --------------------------------";
6.7 +"----------- fun is_contained_in ---------------------------------";
6.8 "-----------------------------------------------------------------";
6.9 "-----------------------------------------------------------------";
6.10
6.11 @@ -513,3 +514,18 @@
6.12 Calculate "op +"] then ()
6.13 else raise error "rewtools.sml filter_appl_rews a + z + 2*a + 3*z + 5 + 6";
6.14
6.15 +
6.16 +"----------- fun is_contained_in ---------------------------------";
6.17 +"----------- fun is_contained_in ---------------------------------";
6.18 +"----------- fun is_contained_in ---------------------------------";
6.19 +val r1 = Thm ("real_diff_minus",num_str real_diff_minus);
6.20 +if contains_rule r1 Test_simplify then ()
6.21 +else raise error "rewtools.sml contains_rule Thm";
6.22 +
6.23 +val r1 = Calc ("op +", eval_binop "#add_");
6.24 +if contains_rule r1 Test_simplify then ()
6.25 +else raise error "rewtools.sml contains_rule Calc";
6.26 +
6.27 +val r1 = Calc ("op -", eval_binop "#add_");
6.28 +if not (contains_rule r1 Test_simplify) then ()
6.29 +else raise error "rewtools.sml contains_rule Calc";
7.1 --- a/src/smltest/ME/script.sml Wed Jan 02 10:06:00 2008 +0100
7.2 +++ b/src/smltest/ME/script.sml Wed Jan 02 14:42:04 2008 +0100
7.3 @@ -231,8 +231,21 @@
7.4 autoCalculate 1 (Step 1);
7.5 val ((pt, p), _) = get_calc 1; show_pt pt;
7.6 show_pt pt;
7.7 -if sel_appl_atomic_tacs pt p =
7.8 +val appltacs = sel_appl_atomic_tacs pt p;
7.9 +if appltacs =
7.10 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
7.11 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
7.12 - Calculate "op *"] then ()
7.13 + Calculate "op *"(*..wrong opID: TODO.WN080102 "times" ok*)] then ()
7.14 else raise error "script.sml fun sel_appl_atomic_tacs diff.behav.";
7.15 +
7.16 +setNextTactic 1 (*p*) (Rewrite_Set "Test_simplify");
7.17 +(*^^^ this tac (= as by autoCalculate !) gives <MESSAGE> ok </MESSAGE>*)
7.18 +
7.19 +(*--------------------- while this vvv (<> as by autoCalculate !) gives
7.20 +
7.21 +> setNextTactic 1 (*p*) (Rewrite ("radd_commute", "?m + ?n = ?n + ?m"));
7.22 +*** upd_env_opt: (None,Subproblem (Test.thy, [linear, univariate, ...]))
7.23 +*** assy: call by ([3], Pbl)
7.24 +
7.25 +applyTactic 1 p (hd appltacs);
7.26 +----------------------------------------------------------------------*)
7.27 \ No newline at end of file