neuper@37906: (* = DiffAppl.ML
neuper@37906:    +++ outcommented tests
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37991: theory' := overwritel (!theory', [("DiffAppl",DiffAppl.thy)]);
neuper@37906: 
neuper@37906: (* 
neuper@37991: > get_pbt ["DiffAppl","maximum_of","function"];
neuper@37991: > get_met ("Script","max_on_interval_by_calculus");
neuper@37906: > !pbltypes;
neuper@37906:   *)
neuper@37906: pbltypes:= overwritel (!pbltypes,
neuper@37906: [
neuper@37906:  prep_pbt DiffAppl.thy
neuper@37991:  (["DiffAppl","maximum_of","function"],
neuper@37906:   [("#Given" ,"fixedValues fix_"),
neuper@37906:    ("#Find"  ,"maximum m_"),
neuper@37906:    ("#Find"  ,"valuesFor vs_"),
neuper@37906:    ("#Relate","relations rs_")  (*,
neuper@37906:    ("#where" ,"foldl (op&) True (map (Not o ((op<=) #0) o Rhs) fix_)"),
neuper@37906:    ("#with"  ,"Ex_frees ((foldl (op &) True rs_) &  \
neuper@37906:     \ (ALL m'. (subst (m_,m') (foldl (op &) True rs_) \
neuper@37906:     \            --> m' <= m_)))")    *)
neuper@37906:   ]),
neuper@37906: 
neuper@37906:  prep_pbt DiffAppl.thy
neuper@37991:  (["DiffAppl","make","function"]:pblID,
neuper@37906:   [("#Given" ,"functionOf f_"),
neuper@37981:    ("#Given" ,"boundVariable v_v"),
neuper@37906:    ("#Given" ,"equalities eqs_"),
neuper@37906:    ("#Find"  ,"functionTerm f_0_")
neuper@37906:   ]),
neuper@37906: 
neuper@37906:  prep_pbt DiffAppl.thy
neuper@37991:  (["DiffAppl","on_interval","maximum_of","function"]:pblID,
neuper@37906:   [("#Given" ,"functionTerm t_"),
neuper@37981:    ("#Given" ,"boundVariable v_v"),
neuper@37906:    ("#Given" ,"interval itv_"),
neuper@37906:    ("#Find"  ,"maxArgument v_0_")
neuper@37906:   ]),
neuper@37906: 
neuper@37906:  prep_pbt DiffAppl.thy
neuper@37991:  (["DiffAppl","find_values","tool"]:pblID,
neuper@37906:   [("#Given" ,"maxArgument ma_"),
neuper@37906:    ("#Given" ,"functionTerm f_"),
neuper@37981:    ("#Given" ,"boundVariable v_v"),
neuper@37906:    ("#Find"  ,"valuesFor vls_"),
neuper@37906:    ("#Relate","additionalRels rs_")
neuper@37906:   ])
neuper@37906: ]);
neuper@37906: 
neuper@37906: 
neuper@37906: methods:= overwritel (!methods,
neuper@37906: [
neuper@37991:  (("DiffAppl","max_by_calculus"):metID,
neuper@37906:   {ppc = prep_met DiffAppl.thy
neuper@37906:    [("#Given" ,"fixedValues fix_"),
neuper@37981:     ("#Given" ,"boundVariable v_v"),
neuper@37906:     ("#Given" ,"interval itv_"),
neuper@37906:     ("#Given" ,"errorBound err_"),
neuper@37906:     ("#Find"  ,"maximum m_"),
neuper@37906:     ("#Find"  ,"valuesFor vs_"),
neuper@37906:     ("#Relate","relations rs_")
neuper@37906:     ],
neuper@37906:    rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
neuper@37906:    scr=EmptyScr} : met),
neuper@37906: 
neuper@37991:  (("DiffAppl","make_fun_by_new_variable"):metID,
neuper@37906:   {ppc = prep_met DiffAppl.thy
neuper@37906:    [("#Given" ,"functionOf f_"),
neuper@37981:     ("#Given" ,"boundVariable v_v"),
neuper@37906:     ("#Given" ,"equalities eqs_"),
neuper@37906:     ("#Find"  ,"functionTerm f_0_")
neuper@37906:     ],
neuper@37906:    rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
neuper@37906:    scr=EmptyScr} : met),
neuper@37906: 
neuper@37991:  (("DiffAppl","make_fun_by_explicit"):metID,
neuper@37906:   {ppc = prep_met DiffAppl.thy
neuper@37906:    [("#Given" ,"functionOf f_"),
neuper@37981:     ("#Given" ,"boundVariable v_v"),
neuper@37906:     ("#Given" ,"equalities eqs_"),
neuper@37906:     ("#Find"  ,"functionTerm f_0_")
neuper@37906:     ],
neuper@37906:    rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
neuper@37906:    scr=EmptyScr} : met),
neuper@37906:   
neuper@37991:  (("DiffAppl","max_on_interval_by_calculus"):metID,
neuper@37906:   {ppc = prep_met DiffAppl.thy
neuper@37906:    [("#Given" ,"functionTerm t_"),
neuper@37981:     ("#Given" ,"boundVariable v_v"),
neuper@37906:     ("#Given" ,"interval itv_"),
neuper@37906:     ("#Given" ,"errorBound err_"),
neuper@37906:     ("#Find"  ,"maxArgument v_0_")
neuper@37906:     ],
neuper@37906:    rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
neuper@37906:    scr=EmptyScr} : met),
neuper@37906: 
neuper@37991:  (("DiffAppl","find_values"):metID,
neuper@37906:   {ppc = prep_met DiffAppl.thy
neuper@37906:    [],
neuper@37906:    rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
neuper@37906:    scr=EmptyScr} : met)
neuper@37906: ]);