1.1 --- a/src/Tools/isac/Build_Isac.thy Wed Sep 08 17:20:03 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Sep 08 17:49:36 2010 +0200
1.3 @@ -78,16 +78,16 @@
1.4 use_thy "Knowledge/Calculus"
1.5 use_thy "Knowledge/Trig"
1.6 use_thy "Knowledge/LogExp"
1.7 -
1.8 use_thy "Knowledge/Diff"
1.9
1.10 -ML {*
1.11 +use_thy "Knowledge/DiffApp"
1.12 +
1.13 +ML {* 111;
1.14 *}
1.15
1.16
1.17 text {*------------------------------------------*}
1.18 (*
1.19 -use_thy "Knowledge/DiffApp"
1.20 use_thy "Knowledge/Integrate"
1.21 use_thy "Knowledge/EqSystem"
1.22 use_thy "Knowledge/Biegelinie"
2.1 --- a/src/Tools/isac/Knowledge/DiffApp-oldscr.sml Wed Sep 08 17:20:03 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/DiffApp-oldscr.sml Wed Sep 08 17:49:36 2010 +0200
2.3 @@ -7,32 +7,32 @@
2.4 ML> ...
2.5 ML> val c = (the o (parse thy)) s;
2.6 val c =
2.7 - "Script1 Maximum_value fix_ m_ rs_ v_v itv_ err_ =
2.8 - let e_e = (hd o filter (Testvar m_)) rs_;
2.9 + "Script1 Maximum_value f_ix m_ r_s v_v itv_ err_ =
2.10 + let e_e = (hd o filter (Testvar m_)) r_s;
2.11 t_ =
2.12 - if #1 < Length rs_
2.13 - then make_fun (R, [make, function], no_met) m_ v_v rs_
2.14 - else (Lhs o hd) rs_;
2.15 + if #1 < Length r_s
2.16 + then make_fun (R, [make, function], no_met) m_ v_v r_s
2.17 + else (Lhs o hd) r_s;
2.18 mx_ =
2.19 max_on_interval (R, [on_interval, max_of, function],
2.20 maximum_on_interval) t_ v_v itv_
2.21 in find_vals (R, [find_values, tool], find_values)
2.22 - mx_ t_ v_v m_ dropWhile (op = e_e) rs_" : cterm
2.23 + mx_ t_ v_v m_ dropWhile (op = e_e) r_s" : cterm
2.24
2.25 ML> set show_types;
2.26 ML> c;
2.27 val c =
2.28 - "Script1 Maximum_value fix_::bool list m_::real rs_::bool list v_v::real itv_v::real set err_::bool =
2.29 - let e_e::bool = (hd o filter (Testvar m_)) rs_;
2.30 + "Script1 Maximum_value f_ix::bool list m_::real r_s::bool list v_v::real itv_v::real set err_::bool =
2.31 + let e_e::bool = (hd o filter (Testvar m_)) r_s;
2.32 t_::real =
2.33 - if (#1::real) < Length rs_
2.34 - then make_fun (R::ID, [make::ID, function::ID], no_met::ID) m_ v_v rs_
2.35 - else (Lhs o hd) rs_;
2.36 + if (#1::real) < Length r_s
2.37 + then make_fun (R::ID, [make::ID, function::ID], no_met::ID) m_ v_v r_s
2.38 + else (Lhs o hd) r_s;
2.39 mx_::real =
2.40 max_on_interval (R, [on_interval::ID, max_of::ID, function],
2.41 maximum_on_interval::ID) t_ v_v itv_
2.42 in find_vals (R, [find_values::ID, tool::ID], find_values)
2.43 - mx_ t_ v_v m_ dropWhile (op = e_e) rs_" : cterm
2.44 + mx_ t_ v_v m_ dropWhile (op = e_e) r_s" : cterm
2.45
2.46
2.47
2.48 @@ -44,20 +44,20 @@
2.49 ML> val c = (the o (parse thy)) s;
2.50 val c =
2.51 "Script maximum =
2.52 - Input [Bool fix_, Real m_, BoolList rs_, Real v_v, RealSet itv_, Bool err_]
2.53 - Local [Bool e_e, Real t_, Real mx_, RealList vs_]
2.54 + Input [Bool f_ix, Real m_, BoolList r_s, Real v_v, RealSet itv_, Bool err_]
2.55 + Local [Bool e_e, Real t_, Real mx_, RealList v_s]
2.56 Tacs [SEQU
2.57 - [let e_e = (hd o filter (Testvar m_)) rs_
2.58 - in if #1 < Length rs_
2.59 + [let e_e = (hd o filter (Testvar m_)) r_s
2.60 + in if #1 < Length r_s
2.61 then Subproblem Spec (R, [make, function], no_met)
2.62 - InOut [In m_, In v_v, In rs_, Out t_]
2.63 - else t_ := (Lhs o hd) rs_ ;
2.64 + InOut [In m_, In v_v, In r_s, Out t_]
2.65 + else t_ := (Lhs o hd) r_s ;
2.66 Subproblem Spec (R, [on_interval, max_of, function],
2.67 maximum_on_interval)
2.68 InOut [In t_, In v_v, In itv_, In err_, Out mx_] ;
2.69 Subproblem Spec (R, [find_values, tool], find_values)
2.70 - InOut [In mx_, In t_, In v_v, In m_, In (dropWhile (op = e_e) rs_),
2.71 - Out vs_]]]
2.72 + InOut [In mx_, In t_, In v_v, In m_, In (dropWhile (op = e_e) r_s),
2.73 + Out v_s]]]
2.74 Return []" : cterm
2.75
2.76 ML> ...
2.77 @@ -65,11 +65,11 @@
2.78 val c =
2.79 "Script make_fun_by_new_variable =
2.80 Input [Real f_f, Real v_v, BoolList eqs]
2.81 - Local [Bool h_, BoolList es_, RealList vs_, Real v1_, Real v2_, Bool e1,
2.82 + Local [Bool h_, BoolList es_, RealList v_s, Real v1_, Real v2_, Bool e1,
2.83 Bool e2_, BoolList s_1, BoolList s_2]
2.84 Tacs [SEQU
2.85 [let h_ = (hd o filter (Testvar m_)) eqs; es_ = eqs -- [h_];
2.86 - vs_ = Var h_ -- [f_]; v1_ = Nth #1 vs_; v2_ = Nth #2 vs_;
2.87 + v_s = Var h_ -- [f_]; v1_ = Nth #1 v_s; v2_ = Nth #2 v_s;
2.88 e1_ = (hd o filter (Testvar v1_)) es_;
2.89 e2_ = (hd o filter (Testvar v2_)) es_
2.90 in Subproblem Spec (R, [univar, equation], no_met)
2.91 @@ -85,10 +85,10 @@
2.92 val c =
2.93 "Script make_fun_explicit =
2.94 Input [Real f_f, Real v_v, BoolList eqs]
2.95 - Local [Bool h_, Bool eq_, RealList vs_, Real v1_, BoolList ss_]
2.96 + Local [Bool h_, Bool eq_, RealList v_s, Real v1_, BoolList ss_]
2.97 Tacs [SEQU
2.98 [let h_ = (hd o filter (Testvar m_)) eqs; eq_ = hd (eqs -- [h_]);
2.99 - vs_ = Var h_ -- [f_]; v1_ = hd (vs_ -- [v_])
2.100 + v_s = Var h_ -- [f_]; v1_ = hd (v_s -- [v_])
2.101 in Subproblem Spec (R, [univar, equation], no_met)
2.102 InOut [In eq_, In v1_, Out ss_]],
2.103 Take (Bool h_) ; Substitute [(v1_, (Rhs o hd) ss_)]]
3.1 --- a/src/Tools/isac/Knowledge/DiffApp.sml Wed Sep 08 17:20:03 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/DiffApp.sml Wed Sep 08 17:49:36 2010 +0200
3.3 @@ -14,13 +14,13 @@
3.4 [
3.5 prep_pbt DiffAppl.thy
3.6 (["DiffAppl","maximum_of","function"],
3.7 - [("#Given" ,"fixedValues fix_"),
3.8 + [("#Given" ,"fixedValues f_ix"),
3.9 ("#Find" ,"maximum m_"),
3.10 - ("#Find" ,"valuesFor vs_"),
3.11 - ("#Relate","relations rs_") (*,
3.12 - ("#where" ,"foldl (op&) True (map (Not o ((op<=) #0) o Rhs) fix_)"),
3.13 - ("#with" ,"Ex_frees ((foldl (op &) True rs_) & \
3.14 - \ (ALL m'. (subst (m_,m') (foldl (op &) True rs_) \
3.15 + ("#Find" ,"valuesFor v_s"),
3.16 + ("#Relate","relations r_s") (*,
3.17 + ("#where" ,"foldl (op&) True (map (Not o ((op<=) #0) o Rhs) f_ix)"),
3.18 + ("#with" ,"Ex_frees ((foldl (op &) True r_s) & \
3.19 + \ (ALL m'. (subst (m_,m') (foldl (op &) True r_s) \
3.20 \ --> m' <= m_)))") *)
3.21 ]),
3.22
3.23 @@ -37,7 +37,7 @@
3.24 [("#Given" ,"functionTerm t_"),
3.25 ("#Given" ,"boundVariable v_v"),
3.26 ("#Given" ,"interval itv_"),
3.27 - ("#Find" ,"maxArgument v_0_")
3.28 + ("#Find" ,"maxArgument v_0")
3.29 ]),
3.30
3.31 prep_pbt DiffAppl.thy
3.32 @@ -46,7 +46,7 @@
3.33 ("#Given" ,"functionTerm f_f"),
3.34 ("#Given" ,"boundVariable v_v"),
3.35 ("#Find" ,"valuesFor vls_"),
3.36 - ("#Relate","additionalRels rs_")
3.37 + ("#Relate","additionalRels r_s")
3.38 ])
3.39 ]);
3.40
3.41 @@ -55,13 +55,13 @@
3.42 [
3.43 (("DiffAppl","max_by_calculus"):metID,
3.44 {ppc = prep_met DiffAppl.thy
3.45 - [("#Given" ,"fixedValues fix_"),
3.46 + [("#Given" ,"fixedValues f_ix"),
3.47 ("#Given" ,"boundVariable v_v"),
3.48 ("#Given" ,"interval itv_"),
3.49 ("#Given" ,"errorBound err_"),
3.50 ("#Find" ,"maximum m_"),
3.51 - ("#Find" ,"valuesFor vs_"),
3.52 - ("#Relate","relations rs_")
3.53 + ("#Find" ,"valuesFor v_s"),
3.54 + ("#Relate","relations r_s")
3.55 ],
3.56 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
3.57 scr=EmptyScr} : met),
3.58 @@ -92,7 +92,7 @@
3.59 ("#Given" ,"boundVariable v_v"),
3.60 ("#Given" ,"interval itv_"),
3.61 ("#Given" ,"errorBound err_"),
3.62 - ("#Find" ,"maxArgument v_0_")
3.63 + ("#Find" ,"maxArgument v_0")
3.64 ],
3.65 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
3.66 scr=EmptyScr} : met),
4.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Wed Sep 08 17:20:03 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Wed Sep 08 17:49:36 2010 +0200
4.3 @@ -29,8 +29,8 @@
4.4 filterVar :: "[real, 'a list] => 'a list"
4.5
4.6 (*primrec*)axioms
4.7 - filterVar_Nil "filterVar v [] = []"
4.8 - filterVar_Const "filterVar v (x#xs) =
4.9 + filterVar_Nil: "filterVar v [] = []"
4.10 + filterVar_Const: "filterVar v (x#xs) =
4.11 (if (v mem (Vars x)) then x#(filterVar v xs)
4.12 else filterVar v xs) "
4.13 text {*WN.6.5.03: old decisions in this file partially are being changed
4.14 @@ -80,16 +80,17 @@
4.15 (!ruleset',
4.16 [("eval_rls",Atools_erls)(*FIXXXME:del with rls.rls'*)
4.17 ]);
4.18 -
4.19 +*}
4.20 +ML{*
4.21
4.22 (** problem types **)
4.23
4.24 store_pbt
4.25 (prep_pbt thy "pbl_fun_max" [] e_pblID
4.26 (["maximum_of","function"],
4.27 - [("#Given" ,["fixedValues fix_"]),
4.28 - ("#Find" ,["maximum m_","valuesFor vs_"]),
4.29 - ("#Relate",["relations rs_"])
4.30 + [("#Given" ,["fixedValues f_ix"]),
4.31 + ("#Find" ,["maximum m_m","valuesFor v_s"]),
4.32 + ("#Relate",["relations r_s"])
4.33 ],
4.34 e_rls, NONE, []));
4.35
4.36 @@ -97,14 +98,14 @@
4.37 (prep_pbt thy "pbl_fun_make" [] e_pblID
4.38 (["make","function"]:pblID,
4.39 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
4.40 - ("#Find" ,["functionEq f_1_"])
4.41 + ("#Find" ,["functionEq f_1"])
4.42 ],
4.43 e_rls, NONE, []));
4.44 store_pbt
4.45 (prep_pbt thy "pbl_fun_max_expl" [] e_pblID
4.46 (["by_explicit","make","function"]:pblID,
4.47 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
4.48 - ("#Find" ,["functionEq f_1_"])
4.49 + ("#Find" ,["functionEq f_1"])
4.50 ],
4.51 e_rls, NONE, [["DiffApp","make_fun_by_explicit"]]));
4.52 store_pbt
4.53 @@ -112,16 +113,16 @@
4.54 (["by_new_variable","make","function"]:pblID,
4.55 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
4.56 (*WN.12.5.03: precond for distinction still missing*)
4.57 - ("#Find" ,["functionEq f_1_"])
4.58 + ("#Find" ,["functionEq f_1"])
4.59 ],
4.60 e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]]));
4.61
4.62 store_pbt
4.63 (prep_pbt thy "pbl_fun_max_interv" [] e_pblID
4.64 (["on_interval","maximum_of","function"]:pblID,
4.65 - [("#Given" ,["functionEq t_","boundVariable v_v","interval itv_"]),
4.66 + [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"]),
4.67 (*WN.12.5.03: precond for distinction still missing*)
4.68 - ("#Find" ,["maxArgument v_0_"])
4.69 + ("#Find" ,["maxArgument v_0"])
4.70 ],
4.71 e_rls, NONE, []));
4.72
4.73 @@ -134,12 +135,14 @@
4.74 store_pbt
4.75 (prep_pbt thy "pbl_tool_findvals" [] e_pblID
4.76 (["find_values","tool"]:pblID,
4.77 - [("#Given" ,["maxArgument ma_","functionEq f_f","boundVariable v_v"]),
4.78 - ("#Find" ,["valuesFor vls_"]),
4.79 - ("#Relate",["additionalRels rs_"])
4.80 + [("#Given" ,["maxArgument m_ax","functionEq f_f","boundVariable v_v"]),
4.81 + ("#Find" ,["valuesFor v_ls"]),
4.82 + ("#Relate",["additionalRels r_s"])
4.83 ],
4.84 e_rls, NONE, []));
4.85
4.86 +*}
4.87 +ML{*
4.88
4.89 (** methods, scripts not yet implemented **)
4.90
4.91 @@ -150,89 +153,99 @@
4.92 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
4.93 crls = Atools_erls, nrls=norm_Rational
4.94 (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
4.95 +*}
4.96 +ML{*
4.97 store_met
4.98 (prep_met thy "met_diffapp_max" [] e_metID
4.99 (["DiffApp","max_by_calculus"]:metID,
4.100 - [("#Given" ,["fixedValues fix_","maximum m_","relations rs_",
4.101 - "boundVariable v_v","interval itv_","errorBound err_"]),
4.102 - ("#Find" ,["valuesFor vs_"]),
4.103 + [("#Given" ,["fixedValues f_ix","maximum m_m","relations r_s",
4.104 + "boundVariable v_v","interval i_tv","errorBound e_rr"]),
4.105 + ("#Find" ,["valuesFor v_s"]),
4.106 ("#Relate",[])
4.107 ],
4.108 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
4.109 crls = eval_rls, nrls=norm_Rational
4.110 (*, asm_rls=[],asm_thm=[]*)},
4.111 - "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list) " ^
4.112 - " (v_v::real) (itv_v::real set) (err_::bool) = " ^
4.113 - " (let e_e = (hd o (filterVar m_)) rs_; " ^
4.114 - " t_ = (if 1 < length_ rs_ " ^
4.115 - " then (SubProblem (DiffApp_,[make,function],[no_met]) " ^
4.116 - " [REAL m_, REAL v_v, BOOL_LIST rs_]) " ^
4.117 - " else (hd rs_)); " ^
4.118 - " (mx_::real) = " ^
4.119 - "SubProblem(DiffApp_,[on_interval,maximum_of,function], " ^
4.120 + "Script Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list) " ^
4.121 + " (v_v::real) (itv_v::real set) (e_rr::bool) = " ^
4.122 + " (let e_e = (hd o (filterVar m_m)) r_s; " ^
4.123 + " t_t = (if 1 < LENGTH r_s " ^
4.124 + " then (SubProblem (DiffApp',[make,function],[no_met]) " ^
4.125 + " [REAL m_m, REAL v_v, BOOL_LIST r_s]) " ^
4.126 + " else (hd r_s)); " ^
4.127 + " (m_x::real) = " ^
4.128 + "SubProblem(DiffApp',[on_interval,maximum_of,function], " ^
4.129 " [DiffApp,max_on_interval_by_calculus]) " ^
4.130 - " [BOOL t_, REAL v_v, REAL_SET itv_] " ^
4.131 - " in ((SubProblem (DiffApp_,[find_values,tool],[Isac,find_values]) " ^
4.132 - " [REAL mx_, REAL (Rhs t_), REAL v_v, REAL m_, " ^
4.133 - " BOOL_LIST (dropWhile (ident e_e) rs_)])::bool list)) "
4.134 + " [BOOL t_t, REAL v_v, REAL_SET i_tv] " ^
4.135 + " in ((SubProblem (DiffApp',[find_values,tool],[Isac,find_values]) " ^
4.136 + " [REAL m_x, REAL (Rhs t_t), REAL v_v, REAL m_m, " ^
4.137 + " BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list)) "
4.138 ));
4.139 +*}
4.140 +ML{*
4.141 store_met
4.142 (prep_met thy "met_diffapp_funnew" [] e_metID
4.143 (["DiffApp","make_fun_by_new_variable"]:metID,
4.144 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
4.145 - ("#Find" ,["functionEq f_1_"])
4.146 + ("#Find" ,["functionEq f_1"])
4.147 ],
4.148 {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls,
4.149 calc=[], crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)},
4.150 "Script Make_fun_by_new_variable (f_f::real) (v_v::real) " ^
4.151 " (eqs::bool list) = " ^
4.152 - "(let h_ = (hd o (filterVar f_)) eqs; " ^
4.153 - " es_ = dropWhile (ident h_) eqs; " ^
4.154 - " vs_ = dropWhile (ident f_) (Vars h_); " ^
4.155 - " v_1 = nth_ 1 vs_; " ^
4.156 - " v_2 = nth_ 2 vs_; " ^
4.157 - " e_1 = (hd o (filterVar v_1)) es_; " ^
4.158 - " e_2 = (hd o (filterVar v_2)) es_; " ^
4.159 + "(let h_h = (hd o (filterVar f_f)) eqs; " ^
4.160 + " e_s = dropWhile (ident h_h) eqs; " ^
4.161 + " v_s = dropWhile (ident f_f) (Vars h_h); " ^
4.162 + " v_1 = NTH 1 v_s; " ^
4.163 + " v_2 = NTH 2 v_s; " ^
4.164 + " e_1 = (hd o (filterVar v_1)) e_s; " ^
4.165 + " e_2 = (hd o (filterVar v_2)) e_s; " ^
4.166 " (s_1::bool list) = " ^
4.167 - " (SubProblem (DiffApp_,[univariate,equation],[no_met])" ^
4.168 + " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^
4.169 " [BOOL e_1, REAL v_1]); " ^
4.170 " (s_2::bool list) = " ^
4.171 - " (SubProblem (DiffApp_,[univariate,equation],[no_met])" ^
4.172 + " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^
4.173 " [BOOL e_2, REAL v_2])" ^
4.174 - "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)"
4.175 + "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)"
4.176 ));
4.177 +*}
4.178 +ML{*
4.179 store_met
4.180 (prep_met thy "met_diffapp_funexp" [] e_metID
4.181 (["DiffApp","make_fun_by_explicit"]:metID,
4.182 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
4.183 - ("#Find" ,["functionEq f_1_"])
4.184 + ("#Find" ,["functionEq f_1"])
4.185 ],
4.186 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
4.187 crls = eval_rls, nrls=norm_Rational
4.188 (*, asm_rls=[],asm_thm=[]*)},
4.189 "Script Make_fun_by_explicit (f_f::real) (v_v::real) " ^
4.190 " (eqs::bool list) = " ^
4.191 - " (let h_ = (hd o (filterVar f_)) eqs; " ^
4.192 - " e_1 = hd (dropWhile (ident h_) eqs); " ^
4.193 - " vs_ = dropWhile (ident f_) (Vars h_); " ^
4.194 - " v_1 = hd (dropWhile (ident v_v) vs_); " ^
4.195 + " (let h_h = (hd o (filterVar f_f)) eqs; " ^
4.196 + " e_1 = hd (dropWhile (ident h_h) eqs); " ^
4.197 + " v_s = dropWhile (ident f_f) (Vars h_h); " ^
4.198 + " v_1 = hd (dropWhile (ident v_v) v_s); " ^
4.199 " (s_1::bool list)= " ^
4.200 - " (SubProblem(DiffApp_,[univariate,equation],[no_met])" ^
4.201 + " (SubProblem(DiffApp',[univariate,equation],[no_met])" ^
4.202 " [BOOL e_1, REAL v_1]) " ^
4.203 - " in Substitute [(v_1 = (rhs o hd) s_1)] h_) "
4.204 + " in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "
4.205 ));
4.206 +*}
4.207 +ML{*
4.208 store_met
4.209 (prep_met thy "met_diffapp_max_oninterval" [] e_metID
4.210 (["DiffApp","max_on_interval_by_calculus"]:metID,
4.211 - [("#Given" ,["functionEq t_","boundVariable v_v","interval itv_"(*,
4.212 - "errorBound err_"*)]),
4.213 - ("#Find" ,["maxArgument v_0_"])
4.214 + [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"(*,
4.215 + "errorBound e_rr"*)]),
4.216 + ("#Find" ,["maxArgument v_0"])
4.217 ],
4.218 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
4.219 crls = eval_rls, nrls=norm_Rational
4.220 (*, asm_rls=[],asm_thm=[]*)},
4.221 "empty_script"
4.222 ));
4.223 +*}
4.224 +ML{*
4.225 store_met
4.226 (prep_met thy "met_diffapp_findvals" [] e_metID
4.227 (["DiffApp","find_values"]:metID,
5.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Sep 08 17:20:03 2010 +0200
5.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Sep 08 17:49:36 2010 +0200
5.3 @@ -415,28 +415,28 @@
5.4 store_pbt
5.5 (prep_pbt thy "pbl_equsys" [] e_pblID
5.6 (["system"],
5.7 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
5.8 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
5.9 ("#Find" ,["solution ss___"](*___ is copy-named*))
5.10 ],
5.11 append_rls "e_rls" e_rls [(*for preds in where_*)],
5.12 - SOME "solveSystem es_ vs_",
5.13 + SOME "solveSystem es_ v_s",
5.14 []));
5.15 store_pbt
5.16 (prep_pbt thy "pbl_equsys_lin" [] e_pblID
5.17 (["linear", "system"],
5.18 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
5.19 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
5.20 (*TODO.WN050929 check linearity*)
5.21 ("#Find" ,["solution ss___"])
5.22 ],
5.23 append_rls "e_rls" e_rls [(*for preds in where_*)],
5.24 - SOME "solveSystem es_ vs_",
5.25 + SOME "solveSystem es_ v_s",
5.26 []));
5.27 store_pbt
5.28 (prep_pbt thy "pbl_equsys_lin_2x2" [] e_pblID
5.29 (["2x2", "linear", "system"],
5.30 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
5.31 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
5.32 - ("#Where" ,["length_ (es_:: bool list) = 2", "length_ vs_ = 2"]),
5.33 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
5.34 + ("#Where" ,["length_ (es_:: bool list) = 2", "length_ v_s = 2"]),
5.35 ("#Find" ,["solution ss___"])
5.36 ],
5.37 append_rls "prls_2x2_linear_system" e_rls
5.38 @@ -445,35 +445,35 @@
5.39 Calc ("op +", eval_binop "#add_"),
5.40 Calc ("op =",eval_equal "#equal_")
5.41 ],
5.42 - SOME "solveSystem es_ vs_",
5.43 + SOME "solveSystem es_ v_s",
5.44 []));
5.45 store_pbt
5.46 (prep_pbt thy "pbl_equsys_lin_2x2_tri" [] e_pblID
5.47 (["triangular", "2x2", "linear", "system"],
5.48 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
5.49 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
5.50 ("#Where" ,
5.51 - ["(tl vs_) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))",
5.52 - " vs_ from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))"]),
5.53 + ["(tl v_s) from_ v_s occur_exactly_in (nth_ 1 (es_::bool list))",
5.54 + " v_s from_ v_s occur_exactly_in (nth_ 2 (es_::bool list))"]),
5.55 ("#Find" ,["solution ss___"])
5.56 ],
5.57 prls_triangular,
5.58 - SOME "solveSystem es_ vs_",
5.59 + SOME "solveSystem es_ v_s",
5.60 [["EqSystem","top_down_substitution","2x2"]]));
5.61 store_pbt
5.62 (prep_pbt thy "pbl_equsys_lin_2x2_norm" [] e_pblID
5.63 (["normalize", "2x2", "linear", "system"],
5.64 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
5.65 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
5.66 ("#Find" ,["solution ss___"])
5.67 ],
5.68 append_rls "e_rls" e_rls [(*for preds in where_*)],
5.69 - SOME "solveSystem es_ vs_",
5.70 + SOME "solveSystem es_ v_s",
5.71 [["EqSystem","normalize","2x2"]]));
5.72 store_pbt
5.73 (prep_pbt thy "pbl_equsys_lin_3x3" [] e_pblID
5.74 (["3x3", "linear", "system"],
5.75 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
5.76 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
5.77 - ("#Where" ,["length_ (es_:: bool list) = 3", "length_ vs_ = 3"]),
5.78 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
5.79 + ("#Where" ,["length_ (es_:: bool list) = 3", "length_ v_s = 3"]),
5.80 ("#Find" ,["solution ss___"])
5.81 ],
5.82 append_rls "prls_3x3_linear_system" e_rls
5.83 @@ -482,14 +482,14 @@
5.84 Calc ("op +", eval_binop "#add_"),
5.85 Calc ("op =",eval_equal "#equal_")
5.86 ],
5.87 - SOME "solveSystem es_ vs_",
5.88 + SOME "solveSystem es_ v_s",
5.89 []));
5.90 store_pbt
5.91 (prep_pbt thy "pbl_equsys_lin_4x4" [] e_pblID
5.92 (["4x4", "linear", "system"],
5.93 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
5.94 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
5.95 - ("#Where" ,["length_ (es_:: bool list) = 4", "length_ vs_ = 4"]),
5.96 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
5.97 + ("#Where" ,["length_ (es_:: bool list) = 4", "length_ v_s = 4"]),
5.98 ("#Find" ,["solution ss___"])
5.99 ],
5.100 append_rls "prls_4x4_linear_system" e_rls
5.101 @@ -498,34 +498,34 @@
5.102 Calc ("op +", eval_binop "#add_"),
5.103 Calc ("op =",eval_equal "#equal_")
5.104 ],
5.105 - SOME "solveSystem es_ vs_",
5.106 + SOME "solveSystem es_ v_s",
5.107 []));
5.108 store_pbt
5.109 (prep_pbt thy "pbl_equsys_lin_4x4_tri" [] e_pblID
5.110 (["triangular", "4x4", "linear", "system"],
5.111 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
5.112 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
5.113 ("#Where" , (*accepts missing variables up to diagional form*)
5.114 - ["(nth_ 1 (vs_::real list)) occurs_in (nth_ 1 (es_::bool list))",
5.115 - "(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))",
5.116 - "(nth_ 3 (vs_::real list)) occurs_in (nth_ 3 (es_::bool list))",
5.117 - "(nth_ 4 (vs_::real list)) occurs_in (nth_ 4 (es_::bool list))"
5.118 + ["(nth_ 1 (v_s::real list)) occurs_in (nth_ 1 (es_::bool list))",
5.119 + "(nth_ 2 (v_s::real list)) occurs_in (nth_ 2 (es_::bool list))",
5.120 + "(nth_ 3 (v_s::real list)) occurs_in (nth_ 3 (es_::bool list))",
5.121 + "(nth_ 4 (v_s::real list)) occurs_in (nth_ 4 (es_::bool list))"
5.122 ]),
5.123 ("#Find" ,["solution ss___"])
5.124 ],
5.125 append_rls "prls_tri_4x4_lin_sys" prls_triangular
5.126 [Calc ("Atools.occurs'_in",eval_occurs_in "")],
5.127 - SOME "solveSystem es_ vs_",
5.128 + SOME "solveSystem es_ v_s",
5.129 [["EqSystem","top_down_substitution","4x4"]]));
5.130
5.131 store_pbt
5.132 (prep_pbt thy "pbl_equsys_lin_4x4_norm" [] e_pblID
5.133 (["normalize", "4x4", "linear", "system"],
5.134 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
5.135 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
5.136 (*length_ is checked 1 level above*)
5.137 ("#Find" ,["solution ss___"])
5.138 ],
5.139 append_rls "e_rls" e_rls [(*for preds in where_*)],
5.140 - SOME "solveSystem es_ vs_",
5.141 + SOME "solveSystem es_ v_s",
5.142 [["EqSystem","normalize","4x4"]]));
5.143
5.144
5.145 @@ -553,10 +553,10 @@
5.146 store_met
5.147 (prep_met thy "met_eqsys_topdown_2x2" [] e_metID
5.148 (["EqSystem","top_down_substitution","2x2"],
5.149 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
5.150 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
5.151 ("#Where" ,
5.152 - ["(tl vs_) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))",
5.153 - " vs_ from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))"]),
5.154 + ["(tl v_s) from_ v_s occur_exactly_in (nth_ 1 (es_::bool list))",
5.155 + " v_s from_ v_s occur_exactly_in (nth_ 2 (es_::bool list))"]),
5.156 ("#Find" ,["solution ss___"])
5.157 ],
5.158 {rew_ord'="ord_simplify_System", rls' = Erls, calc = [],
5.159 @@ -566,19 +566,19 @@
5.160 Thm ("tl_Nil",num_str @{thm tl_Nil})
5.161 ],
5.162 prls = prls_triangular, crls = Erls, nrls = Erls},
5.163 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^
5.164 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^
5.165 " (let e1__ = Take (hd es_); " ^
5.166 -" e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
5.167 +" e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
5.168 " isolate_bdvs False)) @@ " ^
5.169 -" (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
5.170 +" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
5.171 " simplify_System False))) e1__; " ^
5.172 " e2__ = Take (hd (tl es_)); " ^
5.173 " e2__ = ((Substitute [e1__]) @@ " ^
5.174 -" (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
5.175 +" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
5.176 " simplify_System_parenthesized False)) @@ " ^
5.177 -" (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
5.178 +" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
5.179 " isolate_bdvs False)) @@ " ^
5.180 -" (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
5.181 +" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
5.182 " simplify_System False))) e2__; " ^
5.183 " es__ = Take [e1__, e2__] " ^
5.184 " in (Try (Rewrite_Set order_system False)) es__)"
5.185 @@ -587,16 +587,16 @@
5.186 but it does not yet work due to preliminary script-interpreter,
5.187 see eqsystem.sml 'script [EqSystem,top_down_substitution,2x2] Vers.2'
5.188
5.189 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^
5.190 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^
5.191 " (let es__ = Take es_; " ^
5.192 " e1__ = hd es__; " ^
5.193 " e2__ = hd (tl es__); " ^
5.194 " es__ = [e1__, Substitute [e1__] e2__] " ^
5.195 -" in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
5.196 +" in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
5.197 " simplify_System_parenthesized False)) @@ " ^
5.198 -" (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] " ^
5.199 +" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] " ^
5.200 " isolate_bdvs False)) @@ " ^
5.201 -" (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
5.202 +" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
5.203 " simplify_System False))) es__)"
5.204 ---------------------------------------------------------------------------*)
5.205 ));
5.206 @@ -611,7 +611,7 @@
5.207 store_met
5.208 (prep_met thy "met_eqsys_norm_2x2" [] e_metID
5.209 (["EqSystem","normalize","2x2"],
5.210 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
5.211 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
5.212 ("#Find" ,["solution ss___"])],
5.213 {rew_ord'="tless_true", rls' = Erls, calc = [],
5.214 srls = append_rls "srls_normalize_2x2" e_rls
5.215 @@ -620,17 +620,17 @@
5.216 Thm ("tl_Nil",num_str @{thm tl_Nil})
5.217 ],
5.218 prls = Erls, crls = Erls, nrls = Erls},
5.219 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^
5.220 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^
5.221 " (let es__ = ((Try (Rewrite_Set norm_Rational False)) @@ " ^
5.222 -" (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
5.223 +" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
5.224 " simplify_System_parenthesized False)) @@ " ^
5.225 -" (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
5.226 +" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
5.227 " isolate_bdvs False)) @@ " ^
5.228 -" (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
5.229 +" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
5.230 " simplify_System_parenthesized False)) @@ " ^
5.231 " (Try (Rewrite_Set order_system False))) es_ " ^
5.232 " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^
5.233 -" [BOOL_LIST es__, REAL_LIST vs_]))"
5.234 +" [BOOL_LIST es__, REAL_LIST v_s]))"
5.235 ));
5.236
5.237 (*this is for nth_ only*)
5.238 @@ -651,7 +651,7 @@
5.239 store_met
5.240 (prep_met thy "met_eqsys_norm_4x4" [] e_metID
5.241 (["EqSystem","normalize","4x4"],
5.242 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
5.243 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
5.244 ("#Find" ,["solution ss___"])],
5.245 {rew_ord'="tless_true", rls' = Erls, calc = [],
5.246 srls = append_rls "srls_normalize_4x4" srls
5.247 @@ -661,32 +661,32 @@
5.248 ],
5.249 prls = Erls, crls = Erls, nrls = Erls},
5.250 (*GOON met ["EqSystem","normalize","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
5.251 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^
5.252 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^
5.253 " (let es__ = " ^
5.254 " ((Try (Rewrite_Set norm_Rational False)) @@ " ^
5.255 " (Repeat (Rewrite commute_0_equality False)) @@ " ^
5.256 -" (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), " ^
5.257 -" (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] " ^
5.258 +" (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 v_s),(bdv_2, nth_ 2 v_s ), " ^
5.259 +" (bdv_3, nth_ 3 v_s),(bdv_3, nth_ 4 v_s )] " ^
5.260 " simplify_System_parenthesized False)) @@ " ^
5.261 -" (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), " ^
5.262 -" (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] " ^
5.263 +" (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 v_s),(bdv_2, nth_ 2 v_s ), " ^
5.264 +" (bdv_3, nth_ 3 v_s),(bdv_3, nth_ 4 v_s )] " ^
5.265 " isolate_bdvs_4x4 False)) @@ " ^
5.266 -" (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), " ^
5.267 -" (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] " ^
5.268 +" (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 v_s),(bdv_2, nth_ 2 v_s ), " ^
5.269 +" (bdv_3, nth_ 3 v_s),(bdv_3, nth_ 4 v_s )] " ^
5.270 " simplify_System_parenthesized False)) @@ " ^
5.271 " (Try (Rewrite_Set order_system False))) es_ " ^
5.272 " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^
5.273 -" [BOOL_LIST es__, REAL_LIST vs_]))"
5.274 +" [BOOL_LIST es__, REAL_LIST v_s]))"
5.275 ));
5.276 store_met
5.277 (prep_met thy "met_eqsys_topdown_4x4" [] e_metID
5.278 (["EqSystem","top_down_substitution","4x4"],
5.279 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
5.280 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
5.281 ("#Where" , (*accepts missing variables up to diagonal form*)
5.282 - ["(nth_ 1 (vs_::real list)) occurs_in (nth_ 1 (es_::bool list))",
5.283 - "(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))",
5.284 - "(nth_ 3 (vs_::real list)) occurs_in (nth_ 3 (es_::bool list))",
5.285 - "(nth_ 4 (vs_::real list)) occurs_in (nth_ 4 (es_::bool list))"
5.286 + ["(nth_ 1 (v_s::real list)) occurs_in (nth_ 1 (es_::bool list))",
5.287 + "(nth_ 2 (v_s::real list)) occurs_in (nth_ 2 (es_::bool list))",
5.288 + "(nth_ 3 (v_s::real list)) occurs_in (nth_ 3 (es_::bool list))",
5.289 + "(nth_ 4 (v_s::real list)) occurs_in (nth_ 4 (es_::bool list))"
5.290 ]),
5.291 ("#Find" ,["solution ss___"])
5.292 ],
5.293 @@ -696,18 +696,18 @@
5.294 [Calc ("Atools.occurs'_in",eval_occurs_in "")],
5.295 crls = Erls, nrls = Erls},
5.296 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
5.297 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^
5.298 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^
5.299 " (let e1_ = nth_ 1 es_; " ^
5.300 " e2_ = Take (nth_ 2 es_); " ^
5.301 " e2_ = ((Substitute [e1_]) @@ " ^
5.302 -" (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_)," ^
5.303 -" (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]" ^
5.304 +" (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s)," ^
5.305 +" (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]" ^
5.306 " simplify_System_parenthesized False)) @@ " ^
5.307 -" (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_)," ^
5.308 -" (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]" ^
5.309 +" (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s)," ^
5.310 +" (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]" ^
5.311 " isolate_bdvs False)) @@ " ^
5.312 -" (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_)," ^
5.313 -" (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]" ^
5.314 +" (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s)," ^
5.315 +" (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]" ^
5.316 " norm_Rational False))) e2_ " ^
5.317 " in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])"
5.318 ));
6.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Wed Sep 08 17:20:03 2010 +0200
6.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Wed Sep 08 17:49:36 2010 +0200
6.3 @@ -28,7 +28,7 @@
6.4 " #################################################### ";
6.5 " -------------- [maximum_of,function] --------------- ";
6.6 val pbt =
6.7 - ["fixedValues fix_","maximum m_","valuesFor vs_","relations rs_"];
6.8 + ["fixedValues f_ix","maximum m_","valuesFor v_s","relations r_s"];
6.9 map (the o (parseold thy)) pbt;
6.10 val fmz =
6.11 ["fixedValues [r=Arbfix]","maximum A",
6.12 @@ -69,7 +69,7 @@
6.13 " ---- [on_interval,maximum_of,function] ---- ";
6.14 val pbt =
6.15 ["functionTerm t_","boundVariable v_v","interval itv_",
6.16 - "errorBound err_","maxArgument v_0_"];
6.17 + "errorBound err_","maxArgument v_0"];
6.18 map (the o (parseold thy)) pbt;
6.19 val fmz12 =
6.20 [(*28.11.00: "functionTerm (A_0 = a*sqrt(#4*r^^^#2 - a^^^#2))",*)
6.21 @@ -100,7 +100,7 @@
6.22 " --------- [find_values,tool] --------- ";
6.23 val pbt =
6.24 ["maxArgument ma_","functionTerm f_f","boundVariable v_v",
6.25 - "valuesFor vls_","additionalRels rs_"];
6.26 + "valuesFor vls_","additionalRels r_s"];
6.27 map (the o (parseold thy)) pbt;
6.28 val fmz1 =
6.29 ["maxArgument (a_0=(srqt 2)*r)",
6.30 @@ -428,12 +428,12 @@
6.31 val mits = get_obj g_met pt (fst p);
6.32 writeln (itms2str_ ctxt mits);
6.33 (*
6.34 - 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 ()
6.35 + 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 ()
6.36 else raise error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
6.37 *)
6.38 (*FIXME: the environments contain identifers, and NOT values ?!?!?*)
6.39 (* WN051209 while extending 'fun step' for initac, this became better ...
6.40 - 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 ()
6.41 + 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 ()
6.42 else raise error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
6.43 *)
6.44
6.45 @@ -443,25 +443,25 @@
6.46 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
6.47 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
6.48 str2term
6.49 - "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
6.50 + "Script Maximum_value(f_ix::bool list)(m_::real) (r_s::bool list)\
6.51 \ (v_v::real) (itv_v::real set) (err_::bool) = \
6.52 - \ (let e_e = (hd o (filterVar m_)) rs_; \
6.53 - \ t_ = (if 1 < length_ rs_ \
6.54 + \ (let e_e = (hd o (filterVar m_)) r_s; \
6.55 + \ t_ = (if 1 < length_ r_s \
6.56 \ then (SubProblem (Reals_,[make,function],[no_met])\
6.57 - \ [REAL m_, REAL v_v, BOOL_LIST rs_])\
6.58 - \ else (hd rs_)); \
6.59 + \ [REAL m_, REAL v_v, BOOL_LIST r_s])\
6.60 + \ else (hd r_s)); \
6.61 \ (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \
6.62 \ [Isac,maximum_on_interval])\
6.63 \ [BOOL t_, REAL v_v, REAL_SET itv_]\
6.64 \ in ((SubProblem (Reals_,[find_values,tool],[Isac,find_values]) \
6.65 \ [REAL mx_, REAL (Rhs t_), REAL v_v, REAL m_, \
6.66 - \ BOOL_LIST (dropWhile (ident e_e) rs_)])::bool list))";
6.67 + \ BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list))";
6.68
6.69 -val fix_ = (str2term "fix_::bool list",
6.70 +val f_ix = (str2term "f_ix::bool list",
6.71 str2term "[r=Arbfix]");
6.72 val m_ = (str2term "m_::real",
6.73 str2term "A");
6.74 -val rs_ = (str2term "rs_::bool list",
6.75 +val r_s = (str2term "rs_::bool list",
6.76 str2term "[A = a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]");
6.77 val v_v = (str2term "v_v::real",
6.78 str2term "b");
6.79 @@ -469,10 +469,10 @@
6.80 str2term "{x::real. 0 <= x & x <= 2*r}");
6.81 val err_ = (str2term "err_::bool",
6.82 str2term "eps=0");
6.83 -val env = [fix_, m_, rs_ ,v_, itv_, err_];
6.84 +val env = [f_ix, m_, r_s ,v_, itv_, err_];
6.85
6.86 (*--- 1.line in script ---*)
6.87 -val t = str2term "(hd o (filterVar m_)) (rs_::bool list)";
6.88 +val t = str2term "(hd o (filterVar m_)) (r_s::bool list)";
6.89 val s = subst_atomic env t;
6.90 term2str s;
6.91 "(hd o filterVar A) [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
6.92 @@ -482,7 +482,7 @@
6.93 val env = env @ [(str2term "e_::bool",str2term "A = a * b")];
6.94
6.95 (*--- 2.line: condition alone ---*)
6.96 -val t = str2term "1 < length_ (rs_::bool list)";
6.97 +val t = str2term "1 < length_ (r_s::bool list)";
6.98 val s = subst_atomic env t;
6.99 term2str s;
6.100 "1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
6.101 @@ -492,10 +492,10 @@
6.102
6.103 (*--- 2.line in script ---*)
6.104 val t = str2term
6.105 - "(if 1 < length_ rs_ \
6.106 + "(if 1 < length_ r_s \
6.107 \ then (SubProblem (Reals_,[make,function],[no_met])\
6.108 - \ [REAL m_, REAL v_v, BOOL_LIST rs_])\
6.109 - \ else (hd rs_))";
6.110 + \ [REAL m_, REAL v_v, BOOL_LIST r_s])\
6.111 + \ else (hd r_s))";
6.112 val s = subst_atomic env t;
6.113 term2str s;
6.114 "if 1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]\
6.115 @@ -523,8 +523,8 @@
6.116 \ (eqs::bool list) = \
6.117 \ (let h_ = (hd o (filterVar f_)) eqs; \
6.118 \ e_1 = hd (dropWhile (ident h_) eqs); \
6.119 - \ vs_ = dropWhile (ident f_) (Vars h_); \
6.120 - \ v_1 = hd (dropWhile (ident v_v) vs_); \
6.121 + \ v_s = dropWhile (ident f_) (Vars h_); \
6.122 + \ v_1 = hd (dropWhile (ident v_v) v_s); \
6.123 \ (s_1::bool list)=(SubProblem(Reals_,[univar,equation],[no_met])\
6.124 \ [BOOL e_1, REAL v_1])\
6.125 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
6.126 @@ -573,7 +573,7 @@
6.127 val env = env @ [(str2term "vs_::real list", str2term s')];
6.128
6.129 (*--- 4.line in script ---*)
6.130 -val t = str2term "hd (dropWhile (ident v_v) vs_)";
6.131 +val t = str2term "hd (dropWhile (ident v_v) v_s)";
6.132 val s = subst_atomic env t;
6.133 term2str s;
6.134 val t = str2term "hd (dropWhile (ident b) [a, b])";
6.135 @@ -614,9 +614,9 @@
6.136 \ (eqs::bool list) = \
6.137 \(let h_ = (hd o (filterVar f_)) eqs; \
6.138 \ es_ = dropWhile (ident h_) eqs; \
6.139 - \ vs_ = dropWhile (ident f_) (Vars h_); \
6.140 - \ v_1 = nth_ 1 vs_; \
6.141 - \ v_2 = nth_ 2 vs_; \
6.142 + \ v_s = dropWhile (ident f_) (Vars h_); \
6.143 + \ v_1 = nth_ 1 v_s; \
6.144 + \ v_2 = nth_ 2 v_s; \
6.145 \ e_1 = (hd o (filterVar v_1)) es_; \
6.146 \ e_2 = (hd o (filterVar v_2)) es_; \
6.147 \ (s_1::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
6.148 @@ -669,7 +669,7 @@
6.149 val env = env @ [(str2term "vs_::real list", str2term s')];
6.150
6.151 (*--- 4.line in script ---*)
6.152 -val t = str2term "nth_ 1 vs_";
6.153 +val t = str2term "nth_ 1 v_s";
6.154 val s = subst_atomic env t;
6.155 term2str s;
6.156 val t = str2term "nth_ 1 [a, b]";
6.157 @@ -679,7 +679,7 @@
6.158 val env = env @ [(str2term "v_1", str2term s')];
6.159
6.160 (*--- 5.line in script ---*)
6.161 -val t = str2term "nth_ 2 vs_";
6.162 +val t = str2term "nth_ 2 v_s";
6.163 val s = subst_atomic env t;
6.164 term2str s;
6.165 val t = str2term "nth_ 2 [a, b]";
7.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Wed Sep 08 17:20:03 2010 +0200
7.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Wed Sep 08 17:49:36 2010 +0200
7.3 @@ -101,7 +101,7 @@
7.4 atomty (term_of t);
7.5
7.6 val t = str2term
7.7 -"(tl (tl (tl vs_))) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))";
7.8 +"(tl (tl (tl v_s))) from_ v_s occur_exactly_in (nth_ 1 (es_::bool list))";
7.9 atomty t;
7.10 val t = str2term
7.11 "(tl (tl (tl [c,c_2,c_3,c_4]))) from_ [c,c_2,c_3,c_4] occur_exactly_in \
7.12 @@ -284,99 +284,99 @@
7.13 "----------- script [EqSystem,normalize,2x2] ---------------------";
7.14 "----------- script [EqSystem,normalize,2x2] ---------------------";
7.15 val str =
7.16 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.17 -\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.18 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.19 +\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.20 \ simplify_System_parenthesized False) es_ \
7.21 \ in ([]))";
7.22 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.23 val str =
7.24 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.25 -\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.26 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.27 +\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.28 \ simplify_System_parenthesized False) es_ \
7.29 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
7.30 \ []))";
7.31 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.32 val str =
7.33 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.34 -\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.35 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.36 +\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.37 \ simplify_System_parenthesized False) es_ \
7.38 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
7.39 -\ [BOOL_LIST es__, REAL_LIST vs_]))"
7.40 +\ [BOOL_LIST es__, REAL_LIST v_s]))"
7.41 ;
7.42 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.43 val str =
7.44 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.45 -\ (let es__ = Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.46 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.47 +\ (let es__ = Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.48 \ simplify_System_parenthesized False) es_ \
7.49 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
7.50 -\ [BOOL_LIST es__, REAL_LIST vs_]))"
7.51 +\ [BOOL_LIST es__, REAL_LIST v_s]))"
7.52 ;
7.53 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.54 val str =
7.55 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.56 -\ (let es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.57 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.58 +\ (let es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.59 \ simplify_System_parenthesized False)) es_ \
7.60 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
7.61 -\ [BOOL_LIST es__, REAL_LIST vs_]))"
7.62 +\ [BOOL_LIST es__, REAL_LIST v_s]))"
7.63 ;
7.64 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.65 val str =
7.66 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.67 -\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.68 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.69 +\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.70 \ simplify_System_parenthesized False)) @@\
7.71 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.72 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.73 \ simplify_System_parenthesized False))) es_\
7.74 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
7.75 -\ [BOOL_LIST es__, REAL_LIST vs_]))"
7.76 +\ [BOOL_LIST es__, REAL_LIST v_s]))"
7.77 ;
7.78 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.79 val str =
7.80 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.81 -\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.82 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.83 +\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.84 \ simplify_System_parenthesized False)) @@\
7.85 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.86 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.87 \ simplify_System_parenthesized False)) @@\
7.88 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.89 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.90 \ simplify_System_parenthesized False))) es_\
7.91 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
7.92 -\ [BOOL_LIST es__, REAL_LIST vs_]))"
7.93 +\ [BOOL_LIST es__, REAL_LIST v_s]))"
7.94 ;
7.95 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.96 val str =
7.97 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.98 -\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.99 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.100 +\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.101 \ simplify_System_parenthesized False)) @@\
7.102 \ (Try (Rewrite_Set_Inst [] isolate_bdvs False)) @@\
7.103 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.104 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.105 \ simplify_System_parenthesized False)) @@\
7.106 \ (Try (Rewrite_Set order_system False))) es_\
7.107 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
7.108 -\ [BOOL_LIST es__, REAL_LIST vs_]))"
7.109 +\ [BOOL_LIST es__, REAL_LIST v_s]))"
7.110 ;
7.111 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.112 val str =
7.113 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.114 -\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.115 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.116 +\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.117 \ simplify_System_parenthesized False)) @@\
7.118 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_)]\
7.119 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s)]\
7.120 \ isolate_bdvs False)) @@\
7.121 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.122 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.123 \ simplify_System_parenthesized False)) @@\
7.124 \ (Try (Rewrite_Set order_system False))) es_\
7.125 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
7.126 -\ [BOOL_LIST es__, REAL_LIST vs_]))"
7.127 +\ [BOOL_LIST es__, REAL_LIST v_s]))"
7.128 ;
7.129 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.130 val str =
7.131 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.132 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.133 \ (let es__ = ((Try (Rewrite_Set simplify_System_parenthesized False)) @@\
7.134 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.135 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.136 \ isolate_bdvs False)) @@\
7.137 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.138 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.139 \ simplify_System_parenthesized False)) @@\
7.140 \ (Try (Rewrite_Set order_system False))) es_\
7.141 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
7.142 -\ [BOOL_LIST es__, REAL_LIST vs_]))"
7.143 +\ [BOOL_LIST es__, REAL_LIST v_s]))"
7.144 ;
7.145 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.146 (*---^^^-OK-----------------------------------------------------------------*)
7.147 @@ -387,127 +387,127 @@
7.148 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
7.149 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
7.150 val str =
7.151 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.152 -\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.153 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.154 +\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.155 \ simplify_System_parenthesized False) es_ \
7.156 \ in ([]))";
7.157 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.158 val str =
7.159 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.160 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.161 \ (let e1__ = Take (hd es_) \
7.162 \ in ([]))";
7.163 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.164 val str =
7.165 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.166 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.167 \ (let e1__ = Take (hd es_); \
7.168 \ e1__ = Take (hd es_) \
7.169 \ in ([]))";
7.170 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.171 val str =
7.172 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.173 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.174 \ (let e1__ = Take (hd es_); \
7.175 \ e1__ = (Take (hd es_))\
7.176 \ in ([]))";
7.177 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.178 val str =
7.179 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.180 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.181 \ (let e1__ = Take (hd es_); \
7.182 \ e1__ = ((Rewrite_Set order_system False)) e1__\
7.183 \ in ([]))";
7.184 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.185 (*--------------------------------------------------------------------------*)
7.186 val str =
7.187 -"(Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.188 +"(Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.189 \ isolate_bdvs False) (e1__::bool)";
7.190 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.191 (*--------------------------------------------------------------------------*)
7.192 val str =
7.193 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.194 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.195 \ (let e1__ = Take (hd es_); \
7.196 -\ e1__ = ((Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.197 +\ e1__ = ((Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.198 \ isolate_bdvs False)) e1__\
7.199 \ in ([]))";
7.200 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.201 val str =
7.202 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.203 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.204 \ (let e1__ = Take (hd es_); \
7.205 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.206 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.207 \ isolate_bdvs False)) @@\
7.208 -\ (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.209 +\ (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.210 \ simplify_System False)) e1__\
7.211 \ in ([]))";
7.212 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.213 val str =
7.214 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.215 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.216 \ (let e1__ = Take (hd es_); \
7.217 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.218 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.219 \ isolate_bdvs False)) @@\
7.220 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.221 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.222 \ simplify_System False))) e1__\
7.223 \ in ([]))";
7.224 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.225 val str =
7.226 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.227 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.228 \ (let e1__ = Take (hd es_); \
7.229 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.230 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.231 \ isolate_bdvs False)) @@ \
7.232 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.233 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.234 \ simplify_System False))) e1__; \
7.235 \ e2__ = Take (hd (tl es_)) \
7.236 \ in ([]))";
7.237 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.238 val str =
7.239 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.240 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.241 \ (let e1__ = Take (hd es_); \
7.242 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.243 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.244 \ isolate_bdvs False)) @@ \
7.245 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.246 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.247 \ simplify_System False))) e1__; \
7.248 \ e2__ = Take (hd (tl es_)); \
7.249 \ e2__ = Substitute [e1__] e2__ \
7.250 \ in ([]))";
7.251 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.252 val str =
7.253 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.254 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.255 \ (let e1__ = Take (hd es_); \
7.256 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.257 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.258 \ isolate_bdvs False)) @@ \
7.259 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.260 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.261 \ simplify_System False))) e1__; \
7.262 \ e2__ = Take (hd (tl es_)); \
7.263 \ e2__ = ((Substitute [e1__])) e2__ \
7.264 \ in ([]))";
7.265 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.266 val str =
7.267 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.268 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.269 \ (let e1__ = Take (hd es_); \
7.270 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.271 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.272 \ isolate_bdvs False)) @@ \
7.273 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.274 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.275 \ simplify_System False))) e1__; \
7.276 \ e2__ = Take (hd (tl es_)); \
7.277 \ e2__ = ((Substitute [e1__]) @@ \
7.278 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.279 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.280 \ isolate_bdvs False)) @@ \
7.281 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.282 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.283 \ simplify_System False))) e2__ \
7.284 \ in [e1__, e2__])"
7.285 ;
7.286 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.287 val str =
7.288 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.289 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.290 \ (let e1__ = Take (hd es_); \
7.291 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.292 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.293 \ isolate_bdvs False)) @@ \
7.294 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.295 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.296 \ simplify_System False))) e1__; \
7.297 \ e2__ = Take (hd (tl es_)); \
7.298 \ e2__ = ((Substitute [e1__]) @@ \
7.299 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.300 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.301 \ simplify_System_parenthesized False)) @@ \
7.302 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.303 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.304 \ isolate_bdvs False)) @@ \
7.305 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.306 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.307 \ simplify_System False)) @@ \
7.308 \ (Try (Rewrite_Set order_system False))) e2__ \
7.309 \ in [e1__, e2__])"
7.310 @@ -515,19 +515,19 @@
7.311 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.312 (*---^^^-OK-----------------------------------------------------------------*)
7.313 val str =
7.314 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.315 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.316 \ (let e1__ = Take (hd es_); \
7.317 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.318 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.319 \ isolate_bdvs False)) @@ \
7.320 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.321 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.322 \ simplify_System False))) e1__; \
7.323 \ e2__ = Take (hd (tl es_)); \
7.324 \ e2__ = ((Substitute [e1__]) @@ \
7.325 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.326 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.327 \ simplify_System_parenthesized False)) @@ \
7.328 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.329 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.330 \ isolate_bdvs False)) @@ \
7.331 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.332 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.333 \ simplify_System False))) e2__; \
7.334 \ es__ = Take [e1__, e2__]\
7.335 \ in (Try (Rewrite_Set order_system False)) es__)"
7.336 @@ -540,14 +540,14 @@
7.337 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
7.338 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
7.339 val str =
7.340 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.341 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.342 \ (let es__ = Take es_; \
7.343 \ e1__ = hd es__\
7.344 \ in ([]))"
7.345 ;
7.346 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.347 val str =
7.348 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.349 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.350 \ (let es__ = Take es_; \
7.351 \ e1__ = hd es__; \
7.352 \ e2__ = hd (tl es__)\
7.353 @@ -555,7 +555,7 @@
7.354 ;
7.355 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.356 val str =
7.357 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.358 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.359 \ (let es__ = Take es_; \
7.360 \ e1__ = hd es__; \
7.361 \ e2__ = hd (tl es__);\
7.362 @@ -564,7 +564,7 @@
7.363 ;
7.364 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.365 val str =
7.366 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.367 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.368 \ (let es__ = Take es_; \
7.369 \ e1__ = hd es__; \
7.370 \ e2__ = hd (tl es__);\
7.371 @@ -573,87 +573,87 @@
7.372 ;
7.373 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.374 val str =
7.375 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.376 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.377 \ (let es__ = Take es_; \
7.378 \ e1__ = hd es__; \
7.379 \ e2__ = hd (tl es__);\
7.380 \ es__ = [e1__, Substitute [e1__] e2__];\
7.381 -\ es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.382 +\ es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.383 \ simplify_System False)) es__ \
7.384 \ in ([]))"
7.385 ;
7.386 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.387 val str =
7.388 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.389 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.390 \ (let es__ = Take es_; \
7.391 \ e1__ = hd es__; \
7.392 \ e2__ = hd (tl es__);\
7.393 \ es__ = [e1__, Substitute [e1__] e2__];\
7.394 -\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.395 +\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.396 \ isolate_bdvs False)) @@ \
7.397 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.398 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.399 \ simplify_System False))) es__ \
7.400 \ in ([]))"
7.401 ;
7.402 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.403 val str =
7.404 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.405 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.406 \ (let es__ = Take es_; \
7.407 \ e1__ = hd es__; \
7.408 \ e2__ = hd (tl es__);\
7.409 \ es__ = [e1__, Substitute [e1__] e2__];\
7.410 -\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.411 +\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.412 \ simplify_System_parenthesized False)) @@ \
7.413 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.414 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.415 \ isolate_bdvs False)) @@ \
7.416 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.417 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.418 \ simplify_System False))) es__ \
7.419 \ in ([]))"
7.420 ;
7.421 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.422 val str =
7.423 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.424 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.425 \ (let es__ = Take es_; \
7.426 \ e1__ = hd es__; \
7.427 \ e2__ = hd (tl es__); \
7.428 \ es__ = [e1__, Substitute [e1__] e2__]; \
7.429 -\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.430 +\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.431 \ simplify_System_parenthesized False)) @@ \
7.432 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.433 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.434 \ isolate_bdvs False)) @@ \
7.435 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.436 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.437 \ simplify_System False))) es__ \
7.438 \ in es__)"
7.439 ;
7.440 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.441 val str =
7.442 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.443 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.444 \ (let es__ = Take es_; \
7.445 \ e1__ = hd es__; \
7.446 \ e2__ = hd (tl es__); \
7.447 \ es__ = [e1__, Substitute [e1__] e2__] \
7.448 -\ in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.449 +\ in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.450 \ simplify_System_parenthesized False)) @@ \
7.451 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] \
7.452 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] \
7.453 \ isolate_bdvs False)) @@ \
7.454 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.455 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.456 \ simplify_System False))) es__)"
7.457 ;
7.458 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.459 (*---^^^-OK-----------------------------------------------------------------*)
7.460 val str =
7.461 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.462 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.463 \ (let es__ = Take es_; \
7.464 \ e1__ = hd es__; \
7.465 \ e2__ = hd (tl es__); \
7.466 \ es__ = [e1__, Substitute [e1__] e2__] "^
7.467 (* this ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ is a script-'Expr'
7.468 which is not yet searched for 'STac's; thus this script does not yet work*)
7.469 -" in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.470 +" in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.471 \ simplify_System_parenthesized False)) @@ \
7.472 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] \
7.473 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] \
7.474 \ isolate_bdvs False)) @@ \
7.475 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.476 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.477 \ simplify_System False))) es__)"
7.478 ;
7.479 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.480 @@ -791,14 +791,14 @@
7.481 (* val (thy, (pblID, dsc_dats: (string * (string list)) list,
7.482 ev:rls, ca: string option, metIDs:metID list)) =
7.483 (EqSystem.thy, (["system"],
7.484 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
7.485 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
7.486 ("#Find" ,["solution ss___"](*___ is copy-named*))
7.487 ],
7.488 append_rls "e_rls" e_rls [(*for preds in where_*)],
7.489 - SOME "solveSystem es_ vs_",
7.490 + SOME "solveSystem es_ v_s",
7.491 []));
7.492 *)
7.493 -> val [("#Given", [equalities_es_, "solveForVars vs_"])] = gi;
7.494 +> val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
7.495 val equalities_es_ = "equalities es_" : string
7.496 > val (dd, ii) = (split_did o term_of o the o (parse thy)) equalities_es_;
7.497 > show_types:=true; term2str ii; show_types:=false;
7.498 @@ -819,7 +819,7 @@
7.499 [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
7.500 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] ,(es_, [[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
7.501 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]])),
7.502 -(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
7.503 +(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
7.504 (3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
7.505
7.506 > (writeln o pres2str) pre';
7.507 @@ -837,7 +837,7 @@
7.508 ["
7.509 (es_, [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
7.510 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2])","
7.511 -(vs_, [c, c_2])","
7.512 +(v_s, [c, c_2])","
7.513 (ss___, L)"]
7.514
7.515 > val es_ = (fst o hd) env;
7.516 @@ -899,7 +899,7 @@
7.517 (writeln o (itms2str_ (thy2ctxt "Isac"))) probl;
7.518 (*[
7.519 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])),
7.520 -(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
7.521 +(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
7.522 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
7.523 *)
7.524 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
7.525 @@ -968,7 +968,7 @@
7.526 (writeln o (itms2str_ (thy2ctxt "Isac"))) probl;
7.527 (*[
7.528 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])),
7.529 -(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
7.530 +(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
7.531 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
7.532 *)
7.533 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
7.534 @@ -1155,23 +1155,23 @@
7.535 "--- scr [EqSystem,top_down_substitution,4x4] -- a saved trial";
7.536 (*---vvv-this script failed with if ?!?-------------------------------------*)
7.537 val str =
7.538 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.539 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.540 \ (let e1_ = hd es_; \
7.541 -\ v1_ = hd vs_; \
7.542 +\ v1_ = hd v_s; \
7.543 \ xxx = if lhs e1_ =!= v1_ \
7.544 \ then 0=0 \
7.545 \ else let e1_ = Take e1_; \
7.546 -\ e1_ = (Rewrite_Set_Inst [(bdv_1, hd vs_), \
7.547 -\ (bdv_2, hd (tl vs_))] \
7.548 +\ e1_ = (Rewrite_Set_Inst [(bdv_1, hd v_s), \
7.549 +\ (bdv_2, hd (tl v_s))] \
7.550 \ isolate_bdvs False) e1_; \
7.551 \ e2_ = Take (hd (tl es_)); \
7.552 \ e2_ = (Substitute [e1__]) e2_ \
7.553 \ in [e1_, e2_])";
7.554 (*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
7.555 val str =
7.556 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.557 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.558 \ (let e1_ = hd es_; \
7.559 -\ v1_ = hd vs_; \
7.560 +\ v1_ = hd v_s; \
7.561 \ e2_ = Take (hd (tl es_)); \
7.562 \ e2_ = (Substitute [e1__]) e2_ \
7.563 \ in [e1_, e2_])";
7.564 @@ -1179,9 +1179,9 @@
7.565 (*---^^^-OK-----------------------------------------------------------------*)
7.566 (*---vvv-NOT ok-------------------------------------------------------------*)
7.567 val str =
7.568 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.569 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.570 \ (let e1_ = hd es_; \
7.571 -\ v1_ = hd vs_; \
7.572 +\ v1_ = hd v_s; \
7.573 \ xxx = if ((lhs e1_) =!= v1_) then 1 else 2; \
7.574 \ e2_ = Take (hd (tl es_)); \
7.575 \ e2_ = (Substitute [e1__]) e2_ \
7.576 @@ -1196,101 +1196,101 @@
7.577
7.578 "--- scr [EqSystem,top_down_substitution,4x4] -- adapted only to 7.70";
7.579 val str =
7.580 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.581 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.582 \ (let e2__ = Take (hd (tl es_)); \
7.583 \ e2__ = ((Substitute [e1__]) @@ \
7.584 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.585 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.586 \ simplify_System_parenthesized False)) @@ \
7.587 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.588 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.589 \ isolate_bdvs False)) @@ \
7.590 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.591 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.592 \ simplify_System False))) e2__;\
7.593 \ es__ = Take [e1__, e2__] \
7.594 \ in (Try (Rewrite_Set order_system False)) es__)"
7.595 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.596 val str =
7.597 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.598 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.599 \ (let e2__ = Take (nth_ 2 es_); \
7.600 \ e2__ = ((Substitute [e1__]) @@ \
7.601 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.602 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.603 \ simplify_System_parenthesized False)) @@ \
7.604 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.605 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.606 \ isolate_bdvs False)) @@ \
7.607 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
7.608 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
7.609 \ simplify_System False))) e2__;\
7.610 \ es__ = Take [e1__, e2__] \
7.611 \ in (Try (Rewrite_Set order_system False)) es__)"
7.612 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.613 val str =
7.614 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.615 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.616 \ (let e2__ = Take (nth_ 2 es_); \
7.617 \ e2__ = ((Substitute [e1__]) @@ \
7.618 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
7.619 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
7.620 \ simplify_System_parenthesized False)) @@ \
7.621 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)]\
7.622 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]\
7.623 \ isolate_bdvs False)) @@ \
7.624 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)]\
7.625 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]\
7.626 \ simplify_System False))) e2__;\
7.627 \ es__ = Take [e1__, e2__] \
7.628 \ in (Try (Rewrite_Set order_system False)) es__)"
7.629 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.630 val str =
7.631 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.632 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.633 \ (let e2__ = Take (nth_ 2 es_); \
7.634 \ e2__ = ((Substitute [e1__]) @@ \
7.635 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
7.636 -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
7.637 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
7.638 +\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
7.639 \ simplify_System_parenthesized False)) @@ \
7.640 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
7.641 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
7.642 \ isolate_bdvs False)) @@ \
7.643 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
7.644 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
7.645 \ norm_Rational False))) e2__; \
7.646 \ es__ = Take [e1__, e2__] \
7.647 \ in [])"
7.648 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.649 val str =
7.650 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.651 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.652 \ (let e2_ = Take (nth_ 2 es_); \
7.653 \ e2_ = ((Substitute [e1_]) @@ \
7.654 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
7.655 -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
7.656 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
7.657 +\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
7.658 \ simplify_System_parenthesized False)) @@ \
7.659 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
7.660 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
7.661 \ isolate_bdvs False)) @@ \
7.662 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
7.663 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
7.664 \ norm_Rational False))) e2_; \
7.665 \ es_ = Take [e1_, e2_] \
7.666 \ in [e1_, e2_,e3_, e4_])"
7.667 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.668 val str =
7.669 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.670 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.671 \ (let e2_ = Take (nth_ 2 es_); \
7.672 \ e2_ = ((Substitute [e1_]) @@ \
7.673 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
7.674 -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
7.675 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
7.676 +\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
7.677 \ simplify_System_parenthesized False)) @@ \
7.678 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
7.679 -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
7.680 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
7.681 +\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
7.682 \ isolate_bdvs False)) @@ \
7.683 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
7.684 -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
7.685 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
7.686 +\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
7.687 \ norm_Rational False))) e2_; \
7.688 \ es_ = Take [e1_, e2_] \
7.689 \ in [e1_, e2_,e3_, e4_])"
7.690 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.691 (*---^^^-OK-----------------------------------------------------------------*)
7.692 val str =
7.693 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
7.694 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
7.695 \ (let e2_ = Take (nth_ 2 es_); \
7.696 \ e2_ = ((Substitute [e1_]) @@ \
7.697 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
7.698 -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
7.699 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
7.700 +\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
7.701 \ simplify_System_parenthesized False)) @@ \
7.702 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
7.703 -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
7.704 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
7.705 +\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
7.706 \ isolate_bdvs False)) @@ \
7.707 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
7.708 -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
7.709 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
7.710 +\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
7.711 \ norm_Rational False))) e2_ \
7.712 \ in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])"
7.713 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;