wneuper/isa: comparison test/Tools/isac/Knowledge/diffapp.sml

equal deleted inserted replaced

-:eb4c556a525b
+:fac82f29f143
 " #################################################### ";
 "          problemtypes + formalizations               ";
 " #################################################### ";
 " -------------- [maximum_of,function] --------------- ";
 val pbt =
-["fixedValues fix_","maximum m_","valuesFor vs_","relations rs_"];
+["fixedValues f_ix","maximum m_","valuesFor v_s","relations r_s"];
 map (the o (parseold thy)) pbt;
 val fmz =
 ["fixedValues [r=Arbfix]","maximum A",
 "valuesFor [a,b]",
 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
 "solveFor b","solutions b_i"];
 map (the o (parseold thy)) fmz;
 " ---- [on_interval,maximum_of,function] ---- ";
 val pbt =
 ["functionTerm t_","boundVariable v_v","interval itv_",
-"errorBound err_","maxArgument v_0_"];
+"errorBound err_","maxArgument v_0"];
 map (the o (parseold thy)) pbt;
 val fmz12 =
 [(*28.11.00: "functionTerm (A_0 = a*sqrt(#4*r^^^#2 - a^^^#2))",*)
 "functionTerm (a*sqrt(4*r^^^2 - a^^^2))",
 (*28.11.00: "functionTerm (A_0 = b*sqrt(#4*r^^^#2 - b^^^#2))",*)
 (*28.11.00: "derivative (A_0'=Undef)"*)"derivative (Undef)"];
 map (the o (parseold thy)) fmz;
 " --------- [find_values,tool] --------- ";
 val pbt =
 ["maxArgument ma_","functionTerm f_f","boundVariable v_v",
-"valuesFor vls_","additionalRels rs_"];
+"valuesFor vls_","additionalRels r_s"];
 map (the o (parseold thy)) pbt;
 val fmz1 =
 ["maxArgument (a_0=(srqt 2)*r)",
 (*28.11.00: "functionTerm (A_0=a*#2*sqrt r^^^#2 - (a//#2)^^^#2)",*)
 "functionTerm (a*2*sqrt r^^^2 - (a/2)^^^2)",
 fetchProposedTactic 1;
 val ((pt,p),_) = get_calc 1;
 val mits = get_obj g_met pt (fst p);
 writeln (itms2str_ ctxt mits);
 (*
-if itms2str_ ctxt mits = "[\n(1 ,[1] ,true ,#Given ,Cor functionEq (hd rs_) ,(t_, [hd rs_])),\n(2 ,[1] ,true ,#Given ,Cor boundVariable v_v ,(v_, [v_])),\n(3 ,[1] ,true ,#Given ,Cor interval itv_ ,(itv_, [itv_])),\n(4 ,[1] ,true ,#Find ,Cor maxArgument v__0 ,(v_0_, [v__0]))]" then ()
+if itms2str_ ctxt mits = "[\n(1 ,[1] ,true ,#Given ,Cor functionEq (hd r_s) ,(t_, [hd r_s])),\n(2 ,[1] ,true ,#Given ,Cor boundVariable v_v ,(v_, [v_])),\n(3 ,[1] ,true ,#Given ,Cor interval itv_ ,(itv_, [itv_])),\n(4 ,[1] ,true ,#Find ,Cor maxArgument v__0 ,(v_0, [v__0]))]" then ()
 else raise error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
 *)
 (*FIXME: the environments contain identifers, and NOT values ?!?!?*)
 (* WN051209 while extending 'fun step' for initac, this became better ...
-if itms2str_ ctxt 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 ()
+if itms2str_ ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[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] ,(v_s, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(r_s, [[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 ()
 else raise error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
 *)
 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
 str2term
-"Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
+"Script Maximum_value(f_ix::bool list)(m_::real) (r_s::bool list)\
 \      (v_v::real) (itv_v::real set) (err_::bool) =          \
-\ (let e_e = (hd o (filterVar m_)) rs_;              \
+\ (let e_e = (hd o (filterVar m_)) r_s;              \
-\      t_ = (if 1 < length_ rs_                            \
+\      t_ = (if 1 < length_ r_s                            \
 \           then (SubProblem (Reals_,[make,function],[no_met])\
-\                     [REAL m_, REAL v_v, BOOL_LIST rs_])\
+\                     [REAL m_, REAL v_v, BOOL_LIST r_s])\
-\           else (hd rs_));                                \
+\           else (hd r_s));                                \
 \      (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \
 \                                [Isac,maximum_on_interval])\
 \                               [BOOL t_, REAL v_v, REAL_SET itv_]\
 \ in ((SubProblem (Reals_,[find_values,tool],[Isac,find_values])   \
 \      [REAL mx_, REAL (Rhs t_), REAL v_v, REAL m_,     \
-\       BOOL_LIST (dropWhile (ident e_e) rs_)])::bool list))";
+\       BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list))";
-val fix_ = (str2term "fix_::bool list",
+val f_ix = (str2term "f_ix::bool list",
 	    str2term "[r=Arbfix]");
 val m_   = (str2term "m_::real",
 	    str2term "A");
-val rs_  = (str2term "rs_::bool list",
+val r_s  = (str2term "rs_::bool list",
 	    str2term "[A = a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]");
 val v_v   = (str2term "v_v::real",
 	    str2term "b");
 val itv_ = (str2term "itv_v::real set",
 	    str2term "{x::real. 0 <= x & x <= 2*r}");
 val err_ = (str2term "err_::bool",
 	    str2term "eps=0");
-val env = [fix_, m_, rs_ ,v_, itv_, err_];
+val env = [f_ix, m_, r_s ,v_, itv_, err_];
 (*--- 1.line in script ---*)
-val t = str2term "(hd o (filterVar m_)) (rs_::bool list)";
+val t = str2term "(hd o (filterVar m_)) (r_s::bool list)";
 val s = subst_atomic env t;
 term2str s;
 "(hd o filterVar A) [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
 val SOME (s',_) = rewrite_set_ thy false list_rls s;
 val s'' = term2str s';
 if s''="A = a * b" then () else raise error "new behaviour with list_rls 1.1.";
 val env = env @ [(str2term "e_::bool",str2term "A = a * b")];
 (*--- 2.line: condition alone ---*)
-val t = str2term "1 < length_ (rs_::bool list)";
+val t = str2term "1 < length_ (r_s::bool list)";
 val s = subst_atomic env t;
 term2str s;
 "1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
 val SOME (s',_) = rewrite_set_ thy false list_rls s;
 val s'' = term2str s';
 if s''="True" then () else raise error "new behaviour with list_rls 1.2.";
 (*--- 2.line in script ---*)
 val t = str2term
-	    "(if 1 < length_ rs_                            \
+	    "(if 1 < length_ r_s                            \
 \           then (SubProblem (Reals_,[make,function],[no_met])\
-\                     [REAL m_, REAL v_v, BOOL_LIST rs_])\
+\                     [REAL m_, REAL v_v, BOOL_LIST r_s])\
-\           else (hd rs_))";
+\           else (hd r_s))";
 val s = subst_atomic env t;
 term2str s;
 "if 1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]\
 \then SubProblem (Reals_, [make, function], [no_met])\
 \      [REAL A, REAL b,\
 str2term
 "Script Make_fun_by_explicit (f_f::real) (v_v::real)         \
 \      (eqs::bool list) =                                 \
 \ (let h_  = (hd o (filterVar f_)) eqs;                   \
 \      e_1 = hd (dropWhile (ident h_) eqs);               \
-\      vs_ = dropWhile (ident f_) (Vars h_);                \
+\      v_s = dropWhile (ident f_) (Vars h_);                \
-\      v_1 = hd (dropWhile (ident v_v) vs_);                \
+\      v_1 = hd (dropWhile (ident v_v) v_s);                \
 \      (s_1::bool list)=(SubProblem(Reals_,[univar,equation],[no_met])\
 \                          [BOOL e_1, REAL v_1])\
 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
 val f_ = (str2term "f_f::real",
 	  str2term "A");
 val s' = term2str t';
 if s' = "[a, b]" then () else raise error "new behaviour with list_rls 2.3";
 val env = env @ [(str2term "vs_::real list", str2term s')];
 (*--- 4.line in script ---*)
-val t = str2term "hd (dropWhile (ident v_v) vs_)";
+val t = str2term "hd (dropWhile (ident v_v) v_s)";
 val s = subst_atomic env t;
 term2str s;
 val t = str2term "hd (dropWhile (ident b) [a, b])";
 val SOME (t',_) = rewrite_set_ thy false list_rls t;
 val s' = term2str t';
 str2term
 "Script Make_fun_by_new_variable (f_f::real) (v_v::real)     \
 \      (eqs::bool list) =                                 \
 \(let h_ = (hd o (filterVar f_)) eqs;             \
 \     es_ = dropWhile (ident h_) eqs;                    \
-\     vs_ = dropWhile (ident f_) (Vars h_);                \
+\     v_s = dropWhile (ident f_) (Vars h_);                \
-\     v_1 = nth_ 1 vs_;                                   \
+\     v_1 = nth_ 1 v_s;                                   \
-\     v_2 = nth_ 2 vs_;                                   \
+\     v_2 = nth_ 2 v_s;                                   \
 \     e_1 = (hd o (filterVar v_1)) es_;            \
 \     e_2 = (hd o (filterVar v_2)) es_;            \
 \  (s_1::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
 \                    [BOOL e_1, REAL v_1]);\
 \  (s_2::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
 val s' = term2str t';
 if s' = "[a, b]" then () else raise error "new behaviour with list_rls 3.3.";
 val env = env @ [(str2term "vs_::real list", str2term s')];
 (*--- 4.line in script ---*)
-val t = str2term "nth_ 1 vs_";
+val t = str2term "nth_ 1 v_s";
 val s = subst_atomic env t;
 term2str s;
 val t = str2term "nth_ 1 [a, b]";
 val SOME (t',_) = rewrite_set_ thy false list_rls t;
 val s' = term2str t';
 if s' = "a" then () else raise error "new behaviour with list_rls 3.4.";
 val env = env @ [(str2term "v_1", str2term s')];
 (*--- 5.line in script ---*)
-val t = str2term "nth_ 2 vs_";
+val t = str2term "nth_ 2 v_s";
 val s = subst_atomic env t;
 term2str s;
 val t = str2term "nth_ 2 [a, b]";
 val SOME (t',_) = rewrite_set_ thy false list_rls t;
 val s' = term2str t';

branch	isac-update-Isa09-2
changeset 37995	fac82f29f143
parent 37994	eb4c556a525b
child 38031	460c24a6a6ba