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

     1 (* = DiffAppl.ML

     2    +++ outcommented tests

     3 *)

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

     8 (*

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

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

    11 > !pbltypes;

    12   *)

    13 pbltypes:= overwritel (!pbltypes,

    14 [

    15  prep_pbt DiffAppl.thy

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

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

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

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

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

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

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

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

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

    25   ]),

    27  prep_pbt DiffAppl.thy

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

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

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

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

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

    33   ]),

    35  prep_pbt DiffAppl.thy

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

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

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

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

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

    41   ]),

    43  prep_pbt DiffAppl.thy

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

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

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

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

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

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

    50   ])

    51 ]);

    54 methods:= overwritel (!methods,

    55 [

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

    57   {ppc = prep_met DiffAppl.thy

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

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

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

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

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

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

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

    65     ],

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

    67    scr=EmptyScr} : met),

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

    70   {ppc = prep_met DiffAppl.thy

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

    72     ("#Given" ,"boundVariable v_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","make_fun_by_explicit"):metID,

    80   {ppc = prep_met DiffAppl.thy

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

    82     ("#Given" ,"boundVariable v_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","max_on_interval_by_calculus"):metID,

    90   {ppc = prep_met DiffAppl.thy

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

    92     ("#Given" ,"boundVariable v_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","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, 08 Sep 2010 17:49:36 +0200
branch	isac-update-Isa09-2
changeset 37995	fac82f29f143
parent 37994	eb4c556a525b
child 55460	ee6ffa1fc437
permissions	-rw-r--r--