1.1 --- a/test/Tools/isac/Knowledge/algein.sml Fri Jul 22 14:01:52 2011 +0200
1.2 +++ b/test/Tools/isac/Knowledge/algein.sml Mon Jul 25 08:31:53 2011 +0200
1.3 @@ -36,17 +36,7 @@
1.4 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.5 === inhibit exn 110722=============================================================*)
1.6
1.7 -val str =
1.8 -"Script RechnenSymbolScript (k_::bool) (q__::bool) \
1.9 -\(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\
1.10 -\ (let t_ = Take (l_ = Oben + Senkrecht + Unten); \
1.11 -\ sum_ = boollist2sum o_;\
1.12 -\ t_ = Substitute [Oben = sum_] t_;\
1.13 -\ t_ = Substitute o_ t_;\
1.14 -\ t_ = Substitute [k_, q__] t_;\
1.15 -\ t_ = Repeat (Try (Rewrite_Set norm_Poly False)) t_\
1.16 -\ in t_)"
1.17 -;
1.18 +
1.19 (*=== inhibit exn 110722=============================================================
1.20 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.21
2.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Fri Jul 22 14:01:52 2011 +0200
2.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Mon Jul 25 08:31:53 2011 +0200
2.3 @@ -10,7 +10,6 @@
2.4 "table of contents -----------------------------------------------";
2.5 "-----------------------------------------------------------------";
2.6 "----------- the rules -------------------------------------------";
2.7 -"----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
2.8 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
2.9 "----------- simplify_leaf for this script -----------------------";
2.10 "----------- Bsp 7.27 me -----------------------------------------";
2.11 @@ -50,70 +49,7 @@
2.12 else error "biegelinie.sml: Moment_Neigung";
2.13 === inhibit exn 110722=============================================================*)
2.14
2.15 -"----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
2.16 -"----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
2.17 -"----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
2.18 -val str =
2.19 -"Script BiegelinieScript \
2.20 -\(l_::real) (q__::real) (v_v::real) (b_::real=>real) \
2.21 -\(rb_::bool list) (rm_::bool list) = \
2.22 -\ (let q___ = Take (q_ v_v = q__); \
2.23 -\ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \
2.24 -\ (Rewrite Belastung_Querkraft True)) q___; \
2.25 -\ (Q__:: bool) = \
2.26 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
2.27 -\ [diff,integration,named]) \
2.28 -\ [REAL (rhs q___), REAL v_v, real_REAL Q]); \
2.29 -\ Q__ = Rewrite Querkraft_Moment True Q__; \
2.30 -\ (M__::bool) = \
2.31 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
2.32 -\ [diff,integration,named]) \
2.33 -\ [REAL (rhs Q__), REAL v_v, real_REAL M_b]); \
2.34 -\ e1__ = nth_ 1 rm_; \
2.35 -\ (x1__::real) = argument_in (lhs e1__); \
2.36 -\ (M1__::bool) = (Substitute [v_ = x1__]) M__; \
2.37 -\ M1__ = (Substitute [e1__]) M1__ ; \
2.38 -\ M2__ = Take M__; "^
2.39 -(*without this Take 'Substitute [v_ = x2__]' takes _last formula from ctree_*)
2.40 -" e2__ = nth_ 2 rm_; \
2.41 -\ (x2__::real) = argument_in (lhs e2__); \
2.42 -\ (M2__::bool) = ((Substitute [v_ = x2__]) @@ \
2.43 -\ (Substitute [e2__])) M2__; \
2.44 -\ (c_1_2__::bool list) = \
2.45 -\ (SubProblem (Biegelinie_,[linear,system],[no_met]) \
2.46 -\ [booll_ [M1__, M2__], reall [c,c_2]]); \
2.47 -\ M__ = Take M__; \
2.48 -\ M__ = ((Substitute c_1_2__) @@ \
2.49 -\ (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]\
2.50 -\ simplify_System False)) @@ \
2.51 -\ (Rewrite Moment_Neigung False) @@ \
2.52 -\ (Rewrite make_fun_explicit False)) M__; "^
2.53 -(*----------------------- and the same once more ------------------------*)
2.54 -" (N__:: bool) = \
2.55 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
2.56 -\ [diff,integration,named]) \
2.57 -\ [REAL (rhs M__), REAL v_v, real_REAL y']); \
2.58 -\ (B__:: bool) = \
2.59 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
2.60 -\ [diff,integration,named]) \
2.61 -\ [REAL (rhs N__), REAL v_v, real_REAL y]); \
2.62 -\ e1__ = nth_ 1 rb_; \
2.63 -\ (x1__::real) = argument_in (lhs e1__); \
2.64 -\ (B1__::bool) = (Substitute [v_ = x1__]) B__; \
2.65 -\ B1__ = (Substitute [e1__]) B1__ ; \
2.66 -\ B2__ = Take B__; \
2.67 -\ e2__ = nth_ 2 rb_; \
2.68 -\ (x2__::real) = argument_in (lhs e2__); \
2.69 -\ (B2__::bool) = ((Substitute [v_ = x2__]) @@ \
2.70 -\ (Substitute [e2__])) B2__; \
2.71 -\ (c_1_2__::bool list) = \
2.72 -\ (SubProblem (Biegelinie_,[linear,system],[no_met]) \
2.73 -\ [booll_ [B1__, B2__], reall [c,c_2]]); \
2.74 -\ B__ = Take B__; \
2.75 -\ B__ = ((Substitute c_1_2__) @@ \
2.76 -\ (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__ \
2.77 -\ in B__)"
2.78 -;
2.79 +
2.80 (*=== inhibit exn 110722=============================================================
2.81 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.82
2.83 @@ -896,38 +832,6 @@
2.84 \ [BOOL (hd fs_), BOOL b1_]) \
2.85 \ in [e1_,e2_,e3_,e4_])"
2.86 ;
2.87 -(*=== inhibit exn 110722=============================================================
2.88 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.89 -val str =
2.90 -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
2.91 -\ (let b1_ = nth_ 1 rb_; \
2.92 -\ fs_ = filter_sameFunId (lhs b1_) funs_; \
2.93 -\ (e1_::bool) = \
2.94 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
2.95 -\ [Equation,fromFunction]) \
2.96 -\ [BOOL (hd fs_), BOOL b1_]); \
2.97 -\ b2_ = nth_ 2 rb_; \
2.98 -\ fs_ = filter_sameFunId (lhs b2_) funs_; \
2.99 -\ (e2_::bool) = \
2.100 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
2.101 -\ [Equation,fromFunction]) \
2.102 -\ [BOOL (hd fs_), BOOL b2_]); \
2.103 -\ b3_ = nth_ 3 rb_; \
2.104 -\ fs_ = filter_sameFunId (lhs b3_) funs_; \
2.105 -\ (e3_::bool) = \
2.106 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
2.107 -\ [Equation,fromFunction]) \
2.108 -\ [BOOL (hd fs_), BOOL b3_]); \
2.109 -\ b4_ = nth_ 4 rb_; \
2.110 -\ fs_ = filter_sameFunId (lhs b4_) funs_; \
2.111 -\ (e4_::bool) = \
2.112 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
2.113 -\ [Equation,fromFunction]) \
2.114 -\ [BOOL (hd fs_), BOOL b4_]) \
2.115 -\ in [e1_,e2_,e3_,e4_])"
2.116 -;
2.117 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.118 -=== inhibit exn 110722=============================================================*)
2.119
2.120
2.121
3.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Fri Jul 22 14:01:52 2011 +0200
3.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Mon Jul 25 08:31:53 2011 +0200
3.3 @@ -1,3 +1,4 @@
3.4 +
3.5 (* tests for IsacKnowledge/DiffApp
3.6 author Walther Neuper 000301
3.7 (c) due to copyright terms
3.8 @@ -20,7 +21,6 @@
3.9 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
3.10
3.11
3.12 -(*=== inhibit exn 110722=============================================================
3.13
3.14
3.15
3.16 @@ -29,8 +29,10 @@
3.17 " #################################################### ";
3.18 " -------------- [maximum_of,function] --------------- ";
3.19 val pbt =
3.20 - ["fixedValues f_ix","maximum m_","valuesFor v_s","relations r_s"];
3.21 + ["fixedValues f_ix","maximum m_m","valuesFor v_s","relations r_s"];
3.22 +(*=== inhibit exn 110722=============================================================
3.23 map (the o (parseold thy)) pbt;
3.24 +=== inhibit exn 110722=============================================================*)
3.25 val fmz =
3.26 ["fixedValues [r=Arbfix]","maximum A",
3.27 "valuesFor [a,b]",
3.28 @@ -43,11 +45,14 @@
3.29 "interval {x::real. 0 <= x & x <= 2*r}",
3.30 "interval {x::real. 0 <= x & x <= pi}",
3.31 "errorBound (eps=(0::real))"];
3.32 +(*=== inhibit exn 110722=============================================================
3.33 map (the o (parseold thy)) fmz;
3.34 " -------------- [make,function] -------------- ";
3.35 +=== inhibit exn 110722=============================================================*)
3.36 val pbt =
3.37 ["functionOf f_f","boundVariable v_v","equalities eqs",
3.38 - "functionTerm f_0_"];
3.39 + "functionTerm f_0_0"];
3.40 +(*=== inhibit exn 110722=============================================================
3.41 map (the o (parseold thy)) pbt;
3.42 val fmz12 =
3.43 ["functionOf A","boundVariable a","boundVariable b",
3.44 @@ -61,7 +66,7 @@
3.45 map (the o (parseold thy)) fmz3;
3.46 " --------- [univar,equation] --------- ";
3.47 val pbt =
3.48 - ["equality e_e","solveFor v_v","solutions v_i_"];
3.49 + ["equality e_e","solveFor v_v","solutions v_i_i"];
3.50 map (the o (parseold thy)) pbt;
3.51 val fmz =
3.52 ["equality ((a/2)^^^2 + (b/2)^^^2 = r^^^2)",
3.53 @@ -69,8 +74,8 @@
3.54 map (the o (parseold thy)) fmz;
3.55 " ---- [on_interval,maximum_of,function] ---- ";
3.56 val pbt =
3.57 - ["functionTerm t_","boundVariable v_v","interval itv_",
3.58 - "errorBound err_","maxArgument v_0"];
3.59 + ["functionTerm t_t","boundVariable v_v","interval itv_v",
3.60 + "errorBound err_r","maxArgument v_0"];
3.61 map (the o (parseold thy)) pbt;
3.62 val fmz12 =
3.63 [(*28.11.00: "functionTerm (A_0 = a*sqrt(#4*r^^^#2 - a^^^#2))",*)
3.64 @@ -100,8 +105,8 @@
3.65 map (the o (parseold thy)) fmz;
3.66 " --------- [find_values,tool] --------- ";
3.67 val pbt =
3.68 - ["maxArgument ma_","functionTerm f_f","boundVariable v_v",
3.69 - "valuesFor vls_","additionalRels r_s"];
3.70 + ["maxArgument ma_a","functionTerm f_f","boundVariable v_v",
3.71 + "valuesFor vls_s","additionalRels r_s"];
3.72 map (the o (parseold thy)) pbt;
3.73 val fmz1 =
3.74 ["maxArgument (a_0=(srqt 2)*r)",
3.75 @@ -762,3 +767,4 @@
3.76
3.77
3.78 ===== inhibit exn 110722===========================================================*)
3.79 +
4.1 --- a/test/Tools/isac/Test_Some.thy Fri Jul 22 14:01:52 2011 +0200
4.2 +++ b/test/Tools/isac/Test_Some.thy Mon Jul 25 08:31:53 2011 +0200
4.3 @@ -7,13 +7,11 @@
4.4
4.5 ML{* writeln "**** run the test ***************************************" *}
4.6
4.7 -use"../../../test/Tools/isac/Interpret/script.sml"
4.8 +use"../../../test/Tools/isac/Knowledge/biegelinie.sml"
4.9
4.10 ML{*
4.11
4.12
4.13 -
4.14 -
4.15 *}
4.16 ML{*
4.17 *}