neuper@37906: (* application of differential calculus neuper@37954: Walther Neuper 2002 neuper@37954: (c) due to copyright terms neuper@37906: *) neuper@37906: neuper@37954: theory DiffApp imports Diff begin neuper@37906: neuper@37906: consts neuper@37906: neuper@37906: Maximum'_value neuper@37954: :: "[bool list,real,bool list,real,real set,bool, neuper@37954: bool list] => bool list" neuper@37906: ("((Script Maximum'_value (_ _ _ _ _ _ =))// (_))" 9) neuper@37906: neuper@37906: Make'_fun'_by'_new'_variable neuper@37954: :: "[real,real,bool list, neuper@37954: bool] => bool" neuper@37954: ("((Script Make'_fun'_by'_new'_variable (_ _ _ =))// neuper@37954: (_))" 9) neuper@37906: Make'_fun'_by'_explicit neuper@37954: :: "[real,real,bool list, neuper@37954: bool] => bool" neuper@37954: ("((Script Make'_fun'_by'_explicit (_ _ _ =))// neuper@37954: (_))" 9) neuper@37906: neuper@37906: dummy :: real neuper@37906: neuper@37906: (*for script Maximum_value*) neuper@37906: filterVar :: "[real, 'a list] => 'a list" neuper@37906: neuper@37983: (*primrec*)axioms neuper@37995: filterVar_Nil: "filterVar v [] = []" neuper@37995: filterVar_Const: "filterVar v (x#xs) = neuper@37954: (if (v mem (Vars x)) then x#(filterVar v xs) neuper@37954: else filterVar v xs) " neuper@37954: text {*WN.6.5.03: old decisions in this file partially are being changed neuper@37954: in a quick-and-dirty way to make scripts run: Maximum_value, neuper@37954: Make_fun_by_new_variable, Make_fun_by_explicit. neuper@37954: found to be reconsidered: neuper@37954: - descriptions (Descript.thy) neuper@37954: - penv: really need term list; or just rerun the whole example with num/var neuper@37954: - mk_arg, itms2args ... env in script different from penv ? neuper@37954: - L = SubProblem eq ... show some vars on the worksheet ? (other means for neuper@37954: referencing are labels (no on worksheet)) neuper@37954: neuper@37954: WN.6.5.03 quick-and-dirty: mk_arg, itms2args just make most convenient env neuper@37954: from penv as is. neuper@37954: *} neuper@37954: neuper@37954: ML {* neuper@37972: val thy = @{theory}; neuper@37972: neuper@37954: val eval_rls = prep_rls( neuper@37954: Rls {id="eval_rls",preconds = [], rew_ord = ("termlessI",termlessI), neuper@37954: erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*) neuper@37969: rules = [Thm ("refl",num_str @{thm refl}), neuper@37965: Thm ("real_le_refl",num_str @{thm real_le_refl}), neuper@37969: Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}), neuper@37969: Thm ("not_true",num_str @{thm not_true}), neuper@37969: Thm ("not_false",num_str @{thm not_false}), neuper@37969: Thm ("and_true",num_str @{thm and_true}), neuper@37969: Thm ("and_false",num_str @{thm and_false}), neuper@37969: Thm ("or_true",num_str @{thm or_true}), neuper@37969: Thm ("or_false",num_str @{thm or_false}), neuper@37969: Thm ("and_commute",num_str @{thm and_commute}), neuper@37969: Thm ("or_commute",num_str @{thm or_commute}), neuper@37954: neuper@37954: Calc ("op <",eval_equ "#less_"), neuper@37954: Calc ("op <=",eval_equ "#less_equal_"), neuper@37954: neuper@37954: Calc ("Atools.ident",eval_ident "#ident_"), neuper@37954: Calc ("Atools.is'_const",eval_const "#is_const_"), neuper@37954: Calc ("Atools.occurs'_in",eval_occurs_in ""), neuper@37954: Calc ("Tools.matches",eval_matches "") neuper@37954: ], neuper@37954: scr = Script ((term_of o the o (parse thy)) neuper@37954: "empty_script") neuper@37954: }:rls); neuper@37967: ruleset' := overwritelthy @{theory} neuper@37954: (!ruleset', neuper@37954: [("eval_rls",Atools_erls)(*FIXXXME:del with rls.rls'*) neuper@37954: ]); neuper@37995: *} neuper@37995: ML{* neuper@37954: neuper@37954: (** problem types **) neuper@37954: neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_fun_max" [] e_pblID neuper@37954: (["maximum_of","function"], neuper@37995: [("#Given" ,["fixedValues f_ix"]), neuper@37995: ("#Find" ,["maximum m_m","valuesFor v_s"]), neuper@37995: ("#Relate",["relations r_s"]) neuper@37954: ], neuper@37954: e_rls, NONE, [])); neuper@37954: neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_fun_make" [] e_pblID neuper@37954: (["make","function"]:pblID, neuper@37994: [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), neuper@37995: ("#Find" ,["functionEq f_1"]) neuper@37954: ], neuper@37954: e_rls, NONE, [])); neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_fun_max_expl" [] e_pblID neuper@37954: (["by_explicit","make","function"]:pblID, neuper@37994: [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), neuper@37995: ("#Find" ,["functionEq f_1"]) neuper@37954: ], neuper@37954: e_rls, NONE, [["DiffApp","make_fun_by_explicit"]])); neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID neuper@37954: (["by_new_variable","make","function"]:pblID, neuper@37994: [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), neuper@37954: (*WN.12.5.03: precond for distinction still missing*) neuper@37995: ("#Find" ,["functionEq f_1"]) neuper@37954: ], neuper@37954: e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]])); neuper@37954: neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_fun_max_interv" [] e_pblID neuper@37954: (["on_interval","maximum_of","function"]:pblID, neuper@37995: [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"]), neuper@37954: (*WN.12.5.03: precond for distinction still missing*) neuper@37995: ("#Find" ,["maxArgument v_0"]) neuper@37954: ], neuper@37954: e_rls, NONE, [])); neuper@37954: neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_tool" [] e_pblID neuper@37954: (["tool"]:pblID, neuper@37954: [], neuper@37954: e_rls, NONE, [])); neuper@37954: neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_tool_findvals" [] e_pblID neuper@37954: (["find_values","tool"]:pblID, neuper@37995: [("#Given" ,["maxArgument m_ax","functionEq f_f","boundVariable v_v"]), neuper@37995: ("#Find" ,["valuesFor v_ls"]), neuper@37995: ("#Relate",["additionalRels r_s"]) neuper@37954: ], neuper@37954: e_rls, NONE, [])); neuper@37954: neuper@37995: *} neuper@37995: ML{* neuper@37954: neuper@37954: (** methods, scripts not yet implemented **) neuper@37954: neuper@37954: store_met neuper@37972: (prep_met thy "met_diffapp" [] e_metID neuper@37954: (["DiffApp"], neuper@37954: [], neuper@37954: {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, neuper@37954: crls = Atools_erls, nrls=norm_Rational neuper@37954: (*, asm_rls=[],asm_thm=[]*)}, "empty_script")); neuper@37995: *} neuper@37995: ML{* neuper@37954: store_met neuper@37972: (prep_met thy "met_diffapp_max" [] e_metID neuper@37954: (["DiffApp","max_by_calculus"]:metID, neuper@37995: [("#Given" ,["fixedValues f_ix","maximum m_m","relations r_s", neuper@37995: "boundVariable v_v","interval i_tv","errorBound e_rr"]), neuper@37995: ("#Find" ,["valuesFor v_s"]), neuper@37954: ("#Relate",[]) neuper@37954: ], neuper@37954: {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls, neuper@37954: crls = eval_rls, nrls=norm_Rational neuper@37954: (*, asm_rls=[],asm_thm=[]*)}, neuper@37995: "Script Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list) " ^ neuper@37995: " (v_v::real) (itv_v::real set) (e_rr::bool) = " ^ neuper@37995: " (let e_e = (hd o (filterVar m_m)) r_s; " ^ neuper@37995: " t_t = (if 1 < LENGTH r_s " ^ neuper@37995: " then (SubProblem (DiffApp',[make,function],[no_met]) " ^ neuper@37995: " [REAL m_m, REAL v_v, BOOL_LIST r_s]) " ^ neuper@37995: " else (hd r_s)); " ^ neuper@37995: " (m_x::real) = " ^ neuper@37995: "SubProblem(DiffApp',[on_interval,maximum_of,function], " ^ neuper@37954: " [DiffApp,max_on_interval_by_calculus]) " ^ neuper@37995: " [BOOL t_t, REAL v_v, REAL_SET i_tv] " ^ neuper@37995: " in ((SubProblem (DiffApp',[find_values,tool],[Isac,find_values]) " ^ neuper@37995: " [REAL m_x, REAL (Rhs t_t), REAL v_v, REAL m_m, " ^ neuper@37995: " BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list)) " neuper@37954: )); neuper@37995: *} neuper@37995: ML{* neuper@37954: store_met neuper@37972: (prep_met thy "met_diffapp_funnew" [] e_metID neuper@37954: (["DiffApp","make_fun_by_new_variable"]:metID, neuper@37994: [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), neuper@37995: ("#Find" ,["functionEq f_1"]) neuper@37954: ], neuper@37954: {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls, neuper@37954: calc=[], crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)}, neuper@37994: "Script Make_fun_by_new_variable (f_f::real) (v_v::real) " ^ neuper@37994: " (eqs::bool list) = " ^ neuper@37995: "(let h_h = (hd o (filterVar f_f)) eqs; " ^ neuper@37995: " e_s = dropWhile (ident h_h) eqs; " ^ neuper@37995: " v_s = dropWhile (ident f_f) (Vars h_h); " ^ neuper@37995: " v_1 = NTH 1 v_s; " ^ neuper@37995: " v_2 = NTH 2 v_s; " ^ neuper@37995: " e_1 = (hd o (filterVar v_1)) e_s; " ^ neuper@37995: " e_2 = (hd o (filterVar v_2)) e_s; " ^ neuper@37954: " (s_1::bool list) = " ^ neuper@37995: " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^ neuper@37984: " [BOOL e_1, REAL v_1]); " ^ neuper@37954: " (s_2::bool list) = " ^ neuper@37995: " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^ neuper@37984: " [BOOL e_2, REAL v_2])" ^ neuper@37995: "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)" neuper@37954: )); neuper@37995: *} neuper@37995: ML{* neuper@37954: store_met neuper@37972: (prep_met thy "met_diffapp_funexp" [] e_metID neuper@37954: (["DiffApp","make_fun_by_explicit"]:metID, neuper@37994: [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), neuper@37995: ("#Find" ,["functionEq f_1"]) neuper@37954: ], neuper@37954: {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls, neuper@37954: crls = eval_rls, nrls=norm_Rational neuper@37954: (*, asm_rls=[],asm_thm=[]*)}, neuper@37994: "Script Make_fun_by_explicit (f_f::real) (v_v::real) " ^ neuper@37994: " (eqs::bool list) = " ^ neuper@37995: " (let h_h = (hd o (filterVar f_f)) eqs; " ^ neuper@37995: " e_1 = hd (dropWhile (ident h_h) eqs); " ^ neuper@37995: " v_s = dropWhile (ident f_f) (Vars h_h); " ^ neuper@37995: " v_1 = hd (dropWhile (ident v_v) v_s); " ^ neuper@37954: " (s_1::bool list)= " ^ neuper@37995: " (SubProblem(DiffApp',[univariate,equation],[no_met])" ^ neuper@37984: " [BOOL e_1, REAL v_1]) " ^ neuper@37995: " in Substitute [(v_1 = (rhs o hd) s_1)] h_h) " neuper@37954: )); neuper@37995: *} neuper@37995: ML{* neuper@37954: store_met neuper@37972: (prep_met thy "met_diffapp_max_oninterval" [] e_metID neuper@37954: (["DiffApp","max_on_interval_by_calculus"]:metID, neuper@37995: [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"(*, neuper@37995: "errorBound e_rr"*)]), neuper@37995: ("#Find" ,["maxArgument v_0"]) neuper@37954: ], neuper@37954: {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls, neuper@37954: crls = eval_rls, nrls=norm_Rational neuper@37954: (*, asm_rls=[],asm_thm=[]*)}, neuper@37954: "empty_script" neuper@37954: )); neuper@37995: *} neuper@37995: ML{* neuper@37954: store_met neuper@37972: (prep_met thy "met_diffapp_findvals" [] e_metID neuper@37954: (["DiffApp","find_values"]:metID, neuper@37954: [], neuper@37954: {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls, neuper@37954: crls = eval_rls, nrls=norm_Rational(*, neuper@37954: asm_rls=[],asm_thm=[]*)}, neuper@37954: "empty_script")); neuper@37954: neuper@37954: val list_rls = append_rls "list_rls" list_rls neuper@37969: [Thm ("filterVar_Const", num_str @{thm filterVar_Const}), neuper@37969: Thm ("filterVar_Nil", num_str @{thm filterVar_Nil}) neuper@37954: ]; neuper@37967: ruleset' := overwritelthy @{theory} (!ruleset', neuper@37954: [("list_rls",list_rls) neuper@37954: ]); neuper@37954: *} neuper@37906: neuper@37906: end