
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



