wneuper/isa: src/Tools/isac/Knowledge/DiffApp.sml@22235e4dbe5f

     1 (* = DiffAppl.ML

     2    +++ outcommented tests

     3 *)

     6 theory' := overwritel (!theory', [("DiffAppl.thy",DiffAppl.thy)]);

     8 (*

     9 > get_pbt ["DiffAppl.thy","maximum_of","function"];

    10 > get_met ("Script.thy","max_on_interval_by_calculus");

    11 > !pbltypes;

    12   *)

    13 pbltypes:= overwritel (!pbltypes,

    14 [

    15  prep_pbt DiffAppl.thy

    16  (["DiffAppl.thy","maximum_of","function"],

    17   [("#Given" ,"fixedValues fix_"),

    18    ("#Find"  ,"maximum m_"),

    19    ("#Find"  ,"valuesFor vs_"),

    20    ("#Relate","relations rs_")  (*,

    21    ("#where" ,"foldl (op&) True (map (Not o ((op<=) #0) o Rhs) fix_)"),

    22    ("#with"  ,"Ex_frees ((foldl (op &) True rs_) &  \

    23     \ (ALL m'. (subst (m_,m') (foldl (op &) True rs_) \

    24     \            --> m' <= m_)))")    *)

    25   ]),

    27  prep_pbt DiffAppl.thy

    28  (["DiffAppl.thy","make","function"]:pblID,

    29   [("#Given" ,"functionOf f_"),

    30    ("#Given" ,"boundVariable v_"),

    31    ("#Given" ,"equalities eqs_"),

    32    ("#Find"  ,"functionTerm f_0_")

    33   ]),

    35  prep_pbt DiffAppl.thy

    36  (["DiffAppl.thy","on_interval","maximum_of","function"]:pblID,

    37   [("#Given" ,"functionTerm t_"),

    38    ("#Given" ,"boundVariable v_"),

    39    ("#Given" ,"interval itv_"),

    40    ("#Find"  ,"maxArgument v_0_")

    41   ]),

    43  prep_pbt DiffAppl.thy

    44  (["DiffAppl.thy","find_values","tool"]:pblID,

    45   [("#Given" ,"maxArgument ma_"),

    46    ("#Given" ,"functionTerm f_"),

    47    ("#Given" ,"boundVariable v_"),

    48    ("#Find"  ,"valuesFor vls_"),

    49    ("#Relate","additionalRels rs_")

    50   ])

    51 ]);

    54 methods:= overwritel (!methods,

    55 [

    56  (("DiffAppl.thy","max_by_calculus"):metID,

    57   {ppc = prep_met DiffAppl.thy

    58    [("#Given" ,"fixedValues fix_"),

    59     ("#Given" ,"boundVariable v_"),

    60     ("#Given" ,"interval itv_"),

    61     ("#Given" ,"errorBound err_"),

    62     ("#Find"  ,"maximum m_"),

    63     ("#Find"  ,"valuesFor vs_"),

    64     ("#Relate","relations rs_")

    65     ],

    66    rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],

    67    scr=EmptyScr} : met),

    69  (("DiffAppl.thy","make_fun_by_new_variable"):metID,

    70   {ppc = prep_met DiffAppl.thy

    71    [("#Given" ,"functionOf f_"),

    72     ("#Given" ,"boundVariable v_"),

    73     ("#Given" ,"equalities eqs_"),

    74     ("#Find"  ,"functionTerm f_0_")

    75     ],

    76    rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],

    77    scr=EmptyScr} : met),

    79  (("DiffAppl.thy","make_fun_by_explicit"):metID,

    80   {ppc = prep_met DiffAppl.thy

    81    [("#Given" ,"functionOf f_"),

    82     ("#Given" ,"boundVariable v_"),

    83     ("#Given" ,"equalities eqs_"),

    84     ("#Find"  ,"functionTerm f_0_")

    85     ],

    86    rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],

    87    scr=EmptyScr} : met),

    89  (("DiffAppl.thy","max_on_interval_by_calculus"):metID,

    90   {ppc = prep_met DiffAppl.thy

    91    [("#Given" ,"functionTerm t_"),

    92     ("#Given" ,"boundVariable v_"),

    93     ("#Given" ,"interval itv_"),

    94     ("#Given" ,"errorBound err_"),

    95     ("#Find"  ,"maxArgument v_0_")

    96     ],

    97    rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],

    98    scr=EmptyScr} : met),

   100  (("DiffAppl.thy","find_values"):metID,

   101   {ppc = prep_met DiffAppl.thy

   102    [],

   103    rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],

   104    scr=EmptyScr} : met)

   105 ]);

author	Walther Neuper <neuper@ist.tugraz.at>
	Wed, 25 Aug 2010 16:20:07 +0200
branch	isac-update-Isa09-2
changeset 37947	22235e4dbe5f
parent 37906	src/Tools/isac/IsacKnowledge/DiffApp.sml@e2b23ba9df13
child 37981	b2877b9d455a
permissions	-rw-r--r--