1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Knowledge/DiffApp.sml	Wed Aug 25 16:20:07 2010 +0200
     1.3 @@ -0,0 +1,105 @@
     1.4 +(* = DiffAppl.ML
     1.5 +   +++ outcommented tests
     1.6 +*)
     1.7 +
     1.8 +
     1.9 +theory' := overwritel (!theory', [("DiffAppl.thy",DiffAppl.thy)]);
    1.10 +
    1.11 +(* 
    1.12 +> get_pbt ["DiffAppl.thy","maximum_of","function"];
    1.13 +> get_met ("Script.thy","max_on_interval_by_calculus");
    1.14 +> !pbltypes;
    1.15 +  *)
    1.16 +pbltypes:= overwritel (!pbltypes,
    1.17 +[
    1.18 + prep_pbt DiffAppl.thy
    1.19 + (["DiffAppl.thy","maximum_of","function"],
    1.20 +  [("#Given" ,"fixedValues fix_"),
    1.21 +   ("#Find"  ,"maximum m_"),
    1.22 +   ("#Find"  ,"valuesFor vs_"),
    1.23 +   ("#Relate","relations rs_")  (*,
    1.24 +   ("#where" ,"foldl (op&) True (map (Not o ((op<=) #0) o Rhs) fix_)"),
    1.25 +   ("#with"  ,"Ex_frees ((foldl (op &) True rs_) &  \
    1.26 +    \ (ALL m'. (subst (m_,m') (foldl (op &) True rs_) \
    1.27 +    \            --> m' <= m_)))")    *)
    1.28 +  ]),
    1.29 +
    1.30 + prep_pbt DiffAppl.thy
    1.31 + (["DiffAppl.thy","make","function"]:pblID,
    1.32 +  [("#Given" ,"functionOf f_"),
    1.33 +   ("#Given" ,"boundVariable v_"),
    1.34 +   ("#Given" ,"equalities eqs_"),
    1.35 +   ("#Find"  ,"functionTerm f_0_")
    1.36 +  ]),
    1.37 +
    1.38 + prep_pbt DiffAppl.thy
    1.39 + (["DiffAppl.thy","on_interval","maximum_of","function"]:pblID,
    1.40 +  [("#Given" ,"functionTerm t_"),
    1.41 +   ("#Given" ,"boundVariable v_"),
    1.42 +   ("#Given" ,"interval itv_"),
    1.43 +   ("#Find"  ,"maxArgument v_0_")
    1.44 +  ]),
    1.45 +
    1.46 + prep_pbt DiffAppl.thy
    1.47 + (["DiffAppl.thy","find_values","tool"]:pblID,
    1.48 +  [("#Given" ,"maxArgument ma_"),
    1.49 +   ("#Given" ,"functionTerm f_"),
    1.50 +   ("#Given" ,"boundVariable v_"),
    1.51 +   ("#Find"  ,"valuesFor vls_"),
    1.52 +   ("#Relate","additionalRels rs_")
    1.53 +  ])
    1.54 +]);
    1.55 +
    1.56 +
    1.57 +methods:= overwritel (!methods,
    1.58 +[
    1.59 + (("DiffAppl.thy","max_by_calculus"):metID,
    1.60 +  {ppc = prep_met DiffAppl.thy
    1.61 +   [("#Given" ,"fixedValues fix_"),
    1.62 +    ("#Given" ,"boundVariable v_"),
    1.63 +    ("#Given" ,"interval itv_"),
    1.64 +    ("#Given" ,"errorBound err_"),
    1.65 +    ("#Find"  ,"maximum m_"),
    1.66 +    ("#Find"  ,"valuesFor vs_"),
    1.67 +    ("#Relate","relations rs_")
    1.68 +    ],
    1.69 +   rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
    1.70 +   scr=EmptyScr} : met),
    1.71 +
    1.72 + (("DiffAppl.thy","make_fun_by_new_variable"):metID,
    1.73 +  {ppc = prep_met DiffAppl.thy
    1.74 +   [("#Given" ,"functionOf f_"),
    1.75 +    ("#Given" ,"boundVariable v_"),
    1.76 +    ("#Given" ,"equalities eqs_"),
    1.77 +    ("#Find"  ,"functionTerm f_0_")
    1.78 +    ],
    1.79 +   rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
    1.80 +   scr=EmptyScr} : met),
    1.81 +
    1.82 + (("DiffAppl.thy","make_fun_by_explicit"):metID,
    1.83 +  {ppc = prep_met DiffAppl.thy
    1.84 +   [("#Given" ,"functionOf f_"),
    1.85 +    ("#Given" ,"boundVariable v_"),
    1.86 +    ("#Given" ,"equalities eqs_"),
    1.87 +    ("#Find"  ,"functionTerm f_0_")
    1.88 +    ],
    1.89 +   rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
    1.90 +   scr=EmptyScr} : met),
    1.91 +  
    1.92 + (("DiffAppl.thy","max_on_interval_by_calculus"):metID,
    1.93 +  {ppc = prep_met DiffAppl.thy
    1.94 +   [("#Given" ,"functionTerm t_"),
    1.95 +    ("#Given" ,"boundVariable v_"),
    1.96 +    ("#Given" ,"interval itv_"),
    1.97 +    ("#Given" ,"errorBound err_"),
    1.98 +    ("#Find"  ,"maxArgument v_0_")
    1.99 +    ],
   1.100 +   rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
   1.101 +   scr=EmptyScr} : met),
   1.102 +
   1.103 + (("DiffAppl.thy","find_values"):metID,
   1.104 +  {ppc = prep_met DiffAppl.thy
   1.105 +   [],
   1.106 +   rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
   1.107 +   scr=EmptyScr} : met)
   1.108 +]);