1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Knowledge/DiffApp.ML Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,221 @@
1.4 +(* tools for applications of differetiation
1.5 + use"DiffApp.ML";
1.6 + use"Knowledge/DiffApp.ML";
1.7 + use"../Knowledge/DiffApp.ML";
1.8 +
1.9 +
1.10 +WN.6.5.03: old decisions in this file partially are being changed
1.11 + in a quick-and-dirty way to make scripts run: Maximum_value,
1.12 + Make_fun_by_new_variable, Make_fun_by_explicit.
1.13 +found to be reconsidered:
1.14 +- descriptions (Descript.thy)
1.15 +- penv: really need term list; or just rerun the whole example with num/var
1.16 +- mk_arg, itms2args ... env in script different from penv ?
1.17 +- L = SubProblem eq ... show some vars on the worksheet ? (other means for
1.18 + referencing are labels (no on worksheet))
1.19 +
1.20 +WN.6.5.03 quick-and-dirty: mk_arg, itms2args just make most convenient env
1.21 + from penv as is.
1.22 + *)
1.23 +
1.24 +
1.25 +(** interface isabelle -- isac **)
1.26 +
1.27 +theory' := overwritel (!theory', [("DiffApp.thy",DiffApp.thy)]);
1.28 +
1.29 +val eval_rls = prep_rls(
1.30 + Rls {id="eval_rls",preconds = [], rew_ord = ("termlessI",termlessI),
1.31 + erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
1.32 + rules = [Thm ("refl",num_str refl),
1.33 + Thm ("le_refl",num_str le_refl),
1.34 + Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
1.35 + Thm ("not_true",num_str not_true),
1.36 + Thm ("not_false",num_str not_false),
1.37 + Thm ("and_true",and_true),
1.38 + Thm ("and_false",and_false),
1.39 + Thm ("or_true",or_true),
1.40 + Thm ("or_false",or_false),
1.41 + Thm ("and_commute",num_str and_commute),
1.42 + Thm ("or_commute",num_str or_commute),
1.43 +
1.44 + Calc ("op <",eval_equ "#less_"),
1.45 + Calc ("op <=",eval_equ "#less_equal_"),
1.46 +
1.47 + Calc ("Atools.ident",eval_ident "#ident_"),
1.48 + Calc ("Atools.is'_const",eval_const "#is_const_"),
1.49 + Calc ("Atools.occurs'_in",eval_occurs_in ""),
1.50 + Calc ("Tools.matches",eval_matches "")
1.51 + ],
1.52 + scr = Script ((term_of o the o (parse thy))
1.53 + "empty_script")
1.54 + }:rls);
1.55 +ruleset' := overwritelthy thy
1.56 + (!ruleset',
1.57 + [("eval_rls",Atools_erls)(*FIXXXME:del with rls.rls'*)
1.58 + ]);
1.59 +
1.60 +
1.61 +(** problem types **)
1.62 +
1.63 +store_pbt
1.64 + (prep_pbt DiffApp.thy "pbl_fun_max" [] e_pblID
1.65 + (["maximum_of","function"],
1.66 + [("#Given" ,["fixedValues fix_"]),
1.67 + ("#Find" ,["maximum m_","valuesFor vs_"]),
1.68 + ("#Relate",["relations rs_"])
1.69 + ],
1.70 + e_rls, NONE, []));
1.71 +
1.72 +store_pbt
1.73 + (prep_pbt DiffApp.thy "pbl_fun_make" [] e_pblID
1.74 + (["make","function"]:pblID,
1.75 + [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
1.76 + ("#Find" ,["functionEq f_1_"])
1.77 + ],
1.78 + e_rls, NONE, []));
1.79 +store_pbt
1.80 + (prep_pbt DiffApp.thy "pbl_fun_max_expl" [] e_pblID
1.81 + (["by_explicit","make","function"]:pblID,
1.82 + [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
1.83 + ("#Find" ,["functionEq f_1_"])
1.84 + ],
1.85 + e_rls, NONE, [["DiffApp","make_fun_by_explicit"]]));
1.86 +store_pbt
1.87 + (prep_pbt DiffApp.thy "pbl_fun_max_newvar" [] e_pblID
1.88 + (["by_new_variable","make","function"]:pblID,
1.89 + [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
1.90 + (*WN.12.5.03: precond for distinction still missing*)
1.91 + ("#Find" ,["functionEq f_1_"])
1.92 + ],
1.93 + e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]]));
1.94 +
1.95 +store_pbt
1.96 + (prep_pbt DiffApp.thy "pbl_fun_max_interv" [] e_pblID
1.97 + (["on_interval","maximum_of","function"]:pblID,
1.98 + [("#Given" ,["functionEq t_","boundVariable v_","interval itv_"]),
1.99 + (*WN.12.5.03: precond for distinction still missing*)
1.100 + ("#Find" ,["maxArgument v_0_"])
1.101 + ],
1.102 + e_rls, NONE, []));
1.103 +
1.104 +store_pbt
1.105 + (prep_pbt DiffApp.thy "pbl_tool" [] e_pblID
1.106 + (["tool"]:pblID,
1.107 + [],
1.108 + e_rls, NONE, []));
1.109 +
1.110 +store_pbt
1.111 + (prep_pbt DiffApp.thy "pbl_tool_findvals" [] e_pblID
1.112 + (["find_values","tool"]:pblID,
1.113 + [("#Given" ,["maxArgument ma_","functionEq f_","boundVariable v_"]),
1.114 + ("#Find" ,["valuesFor vls_"]),
1.115 + ("#Relate",["additionalRels rs_"])
1.116 + ],
1.117 + e_rls, NONE, []));
1.118 +
1.119 +
1.120 +(** methods, scripts not yet implemented **)
1.121 +
1.122 +store_met
1.123 + (prep_met Diff.thy "met_diffapp" [] e_metID
1.124 + (["DiffApp"],
1.125 + [],
1.126 + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
1.127 + crls = Atools_erls, nrls=norm_Rational
1.128 + (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
1.129 +store_met
1.130 + (prep_met DiffApp.thy "met_diffapp_max" [] e_metID
1.131 + (["DiffApp","max_by_calculus"]:metID,
1.132 + [("#Given" ,["fixedValues fix_","maximum m_","relations rs_",
1.133 + "boundVariable v_","interval itv_","errorBound err_"]),
1.134 + ("#Find" ,["valuesFor vs_"]),
1.135 + ("#Relate",[])
1.136 + ],
1.137 + {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
1.138 + crls = eval_rls, nrls=norm_Rational
1.139 + (*, asm_rls=[],asm_thm=[]*)},
1.140 + "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
1.141 + \ (v_::real) (itv_::real set) (err_::bool) = \
1.142 + \ (let e_ = (hd o (filterVar m_)) rs_; \
1.143 + \ t_ = (if 1 < length_ rs_ \
1.144 + \ then (SubProblem (DiffApp_,[make,function],[no_met])\
1.145 + \ [real_ m_, real_ v_, bool_list_ rs_])\
1.146 + \ else (hd rs_)); \
1.147 + \ (mx_::real) = SubProblem(DiffApp_,[on_interval,maximum_of,function],\
1.148 + \ [DiffApp,max_on_interval_by_calculus])\
1.149 + \ [bool_ t_, real_ v_, real_set_ itv_]\
1.150 + \ in ((SubProblem (DiffApp_,[find_values,tool],[Isac,find_values]) \
1.151 + \ [real_ mx_, real_ (Rhs t_), real_ v_, real_ m_, \
1.152 + \ bool_list_ (dropWhile (ident e_) rs_)])::bool list))"
1.153 + ));
1.154 +store_met
1.155 + (prep_met DiffApp.thy "met_diffapp_funnew" [] e_metID
1.156 + (["DiffApp","make_fun_by_new_variable"]:metID,
1.157 + [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
1.158 + ("#Find" ,["functionEq f_1_"])
1.159 + ],
1.160 + {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls,
1.161 + calc=[], crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)},
1.162 + "Script Make_fun_by_new_variable (f_::real) (v_::real) \
1.163 + \ (eqs_::bool list) = \
1.164 + \(let h_ = (hd o (filterVar f_)) eqs_; \
1.165 + \ es_ = dropWhile (ident h_) eqs_; \
1.166 + \ vs_ = dropWhile (ident f_) (Vars h_); \
1.167 + \ v_1 = nth_ 1 vs_; \
1.168 + \ v_2 = nth_ 2 vs_; \
1.169 + \ e_1 = (hd o (filterVar v_1)) es_; \
1.170 + \ e_2 = (hd o (filterVar v_2)) es_; \
1.171 + \ (s_1::bool list) = (SubProblem (DiffApp_,[univariate,equation],[no_met])\
1.172 + \ [bool_ e_1, real_ v_1]);\
1.173 + \ (s_2::bool list) = (SubProblem (DiffApp_,[univariate,equation],[no_met])\
1.174 + \ [bool_ e_2, real_ v_2])\
1.175 + \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)"
1.176 +));
1.177 +store_met
1.178 +(prep_met DiffApp.thy "met_diffapp_funexp" [] e_metID
1.179 +(["DiffApp","make_fun_by_explicit"]:metID,
1.180 + [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
1.181 + ("#Find" ,["functionEq f_1_"])
1.182 + ],
1.183 + {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
1.184 + crls = eval_rls, nrls=norm_Rational
1.185 + (*, asm_rls=[],asm_thm=[]*)},
1.186 + "Script Make_fun_by_explicit (f_::real) (v_::real) \
1.187 + \ (eqs_::bool list) = \
1.188 + \ (let h_ = (hd o (filterVar f_)) eqs_; \
1.189 + \ e_1 = hd (dropWhile (ident h_) eqs_); \
1.190 + \ vs_ = dropWhile (ident f_) (Vars h_); \
1.191 + \ v_1 = hd (dropWhile (ident v_) vs_); \
1.192 + \ (s_1::bool list)=(SubProblem(DiffApp_,[univariate,equation],[no_met])\
1.193 + \ [bool_ e_1, real_ v_1])\
1.194 + \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)"
1.195 + ));
1.196 +store_met
1.197 + (prep_met DiffApp.thy "met_diffapp_max_oninterval" [] e_metID
1.198 + (["DiffApp","max_on_interval_by_calculus"]:metID,
1.199 + [("#Given" ,["functionEq t_","boundVariable v_","interval itv_"(*,
1.200 + "errorBound err_"*)]),
1.201 + ("#Find" ,["maxArgument v_0_"])
1.202 + ],
1.203 + {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
1.204 + crls = eval_rls, nrls=norm_Rational
1.205 + (*, asm_rls=[],asm_thm=[]*)},
1.206 + "empty_script"
1.207 + ));
1.208 +store_met
1.209 + (prep_met DiffApp.thy "met_diffapp_findvals" [] e_metID
1.210 + (["DiffApp","find_values"]:metID,
1.211 + [],
1.212 + {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
1.213 + crls = eval_rls, nrls=norm_Rational(*,
1.214 + asm_rls=[],asm_thm=[]*)},
1.215 + "empty_script"));
1.216 +
1.217 +val list_rls = append_rls "list_rls" list_rls
1.218 + [Thm ("filterVar_Const", num_str filterVar_Const),
1.219 + Thm ("filterVar_Nil", num_str filterVar_Nil)
1.220 + ];
1.221 +ruleset' := overwritelthy thy (!ruleset',
1.222 + [("list_rls",list_rls)
1.223 + ]);
1.224 +