Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Knowledge/DiffApp.sml
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 08 Sep 2010 16:47:22 +0200
branchisac-update-Isa09-2
changeset 37991 028442673981
parent 37981 b2877b9d455a
child 37994 eb4c556a525b
permissions -rw-r--r--
tuned src + test

find . -type f -exec sed -i s/nadd_divide_distrib/add_divide_distrib/g {} \;
find . -type f -exec sed -i s/"\.thy\""/"\""/g {} \;
find . -type f -exec sed -i s/" indexname_ord"/" Term_Ord.indexname_ord"/g {} \;
find . -type f -exec sed -i s/"(string_of_cterm o cterm_of(sign_of thy))"/"(Syntax.string_of_term (thy2ctxt thy))"/g {} \;
find . -type f -exec sed -i s/" L_"/" L_L"/g {} \;
find . -type f -exec sed -i s/" L_:"/" L_L:"/g {} \;
find . -type f -exec sed -i s/"e_;"/"e_e;"/g {} \;
find . -type f -exec sed -i s/"v_)"/"v_v)"/g {} \;
find . -type f -exec sed -i s/"v_:"/"v_v:"/g {} \; 
     1 (* = DiffAppl.ML

     2    +++ outcommented tests

     3 *)

     4 

     5 

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

     7 

     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 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   ]),

    26 

    27  prep_pbt DiffAppl.thy

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

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

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

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

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

    33   ]),

    34 

    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   ]),

    42 

    43  prep_pbt DiffAppl.thy

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

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

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

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

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

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

    50   ])

    51 ]);

    52 

    53 

    54 methods:= overwritel (!methods,

    55 [

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

    57   {ppc = prep_met DiffAppl.thy

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

    59     ("#Given" ,"boundVariable v_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),

    68 

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

    70   {ppc = prep_met DiffAppl.thy

    71    [("#Given" ,"functionOf 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),

    78 

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

    80   {ppc = prep_met DiffAppl.thy

    81    [("#Given" ,"functionOf 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),

    88   

    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),

    99 

   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 ]);
wneuper/isa