1.1 --- a/src/Tools/isac/IsacKnowledge/DiffApp.ML Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,221 +0,0 @@
1.4 -(* tools for applications of differetiation
1.5 - use"DiffApp.ML";
1.6 - use"IsacKnowledge/DiffApp.ML";
1.7 - use"../IsacKnowledge/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 -