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.ML
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 25 Aug 2010 16:20:07 +0200
branchisac-update-Isa09-2
changeset 37947 22235e4dbe5f
parent 37926 src/Tools/isac/IsacKnowledge/DiffApp.ML@e6fc98fbcb85
child 37952 9ddd1000b900
permissions -rw-r--r--
renamed isac's directories and Build_Isac.thy

Scripts --> ProgLang
ME --> Interpret
IsacKnowledge --> Knowledge 
     1 (* tools for applications of differetiation

     2  use"DiffApp.ML";

     3  use"Knowledge/DiffApp.ML";

     4  use"../Knowledge/DiffApp.ML";

     5 

     6 

     7 WN.6.5.03: old decisions in this file partially are being changed

     8   in a quick-and-dirty way to make scripts run: Maximum_value,

     9   Make_fun_by_new_variable, Make_fun_by_explicit.

    10 found to be reconsidered:

    11 - descriptions (Descript.thy)

    12 - penv: really need term list; or just rerun the whole example with num/var

    13 - mk_arg, itms2args ... env in script different from penv ?

    14 - L = SubProblem eq ... show some vars on the worksheet ? (other means for

    15   referencing are labels (no on worksheet))

    16 

    17 WN.6.5.03 quick-and-dirty: mk_arg, itms2args just make most convenient env

    18   from penv as is.    

    19  *)

    20 

    21 

    22 (** interface isabelle -- isac **)

    23 

    24 theory' := overwritel (!theory', [("DiffApp.thy",DiffApp.thy)]);

    25 

    26 val eval_rls = prep_rls(

    27   Rls {id="eval_rls",preconds = [], rew_ord = ("termlessI",termlessI), 

    28       erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)

    29       rules = [Thm ("refl",num_str refl),

    30 		Thm ("le_refl",num_str le_refl),

    31 		Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),

    32 		Thm ("not_true",num_str not_true),

    33 		Thm ("not_false",num_str not_false),

    34 		Thm ("and_true",and_true),

    35 		Thm ("and_false",and_false),

    36 		Thm ("or_true",or_true),

    37 		Thm ("or_false",or_false),

    38 		Thm ("and_commute",num_str and_commute),

    39 		Thm ("or_commute",num_str or_commute),

    40 		

    41 		Calc ("op <",eval_equ "#less_"),

    42 		Calc ("op <=",eval_equ "#less_equal_"),

    43 		

    44 		Calc ("Atools.ident",eval_ident "#ident_"),    

    45 		Calc ("Atools.is'_const",eval_const "#is_const_"),

    46 		Calc ("Atools.occurs'_in",eval_occurs_in ""),    

    47 		Calc ("Tools.matches",eval_matches "")

    48 	       ],

    49       scr = Script ((term_of o the o (parse thy)) 

    50       "empty_script")

    51       }:rls);

    52 ruleset' := overwritelthy thy

    53 		(!ruleset',

    54 		 [("eval_rls",Atools_erls)(*FIXXXME:del with rls.rls'*)

    55 		  ]);

    56 

    57 

    58 (** problem types **)

    59 

    60 store_pbt

    61  (prep_pbt DiffApp.thy "pbl_fun_max" [] e_pblID

    62  (["maximum_of","function"],

    63   [("#Given" ,["fixedValues fix_"]),

    64    ("#Find"  ,["maximum m_","valuesFor vs_"]),

    65    ("#Relate",["relations rs_"])

    66   ],

    67   e_rls, NONE, []));

    68 

    69 store_pbt

    70  (prep_pbt DiffApp.thy "pbl_fun_make" [] e_pblID

    71  (["make","function"]:pblID,

    72   [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),

    73    ("#Find"  ,["functionEq f_1_"])

    74   ],

    75   e_rls, NONE, []));

    76 store_pbt

    77  (prep_pbt DiffApp.thy "pbl_fun_max_expl" [] e_pblID

    78  (["by_explicit","make","function"]:pblID,

    79   [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),

    80    ("#Find"  ,["functionEq f_1_"])

    81   ],

    82   e_rls, NONE, [["DiffApp","make_fun_by_explicit"]]));

    83 store_pbt

    84  (prep_pbt DiffApp.thy "pbl_fun_max_newvar" [] e_pblID

    85  (["by_new_variable","make","function"]:pblID,

    86   [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),

    87    (*WN.12.5.03: precond for distinction still missing*)

    88    ("#Find"  ,["functionEq f_1_"])

    89   ],

    90   e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]]));

    91 

    92 store_pbt

    93  (prep_pbt DiffApp.thy "pbl_fun_max_interv" [] e_pblID

    94  (["on_interval","maximum_of","function"]:pblID,

    95   [("#Given" ,["functionEq t_","boundVariable v_","interval itv_"]),

    96    (*WN.12.5.03: precond for distinction still missing*)

    97    ("#Find"  ,["maxArgument v_0_"])

    98   ],

    99   e_rls, NONE, []));

   100 

   101 store_pbt

   102  (prep_pbt DiffApp.thy "pbl_tool" [] e_pblID

   103  (["tool"]:pblID,

   104   [],

   105   e_rls, NONE, []));

   106 

   107 store_pbt

   108  (prep_pbt DiffApp.thy "pbl_tool_findvals" [] e_pblID

   109  (["find_values","tool"]:pblID,

   110   [("#Given" ,["maxArgument ma_","functionEq f_","boundVariable v_"]),

   111    ("#Find"  ,["valuesFor vls_"]),

   112    ("#Relate",["additionalRels rs_"])

   113   ],

   114   e_rls, NONE, []));

   115 

   116 

   117 (** methods, scripts not yet implemented **)

   118 

   119 store_met

   120  (prep_met Diff.thy "met_diffapp" [] e_metID

   121  (["DiffApp"],

   122    [],

   123    {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,

   124     crls = Atools_erls, nrls=norm_Rational

   125     (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));

   126 store_met

   127  (prep_met DiffApp.thy "met_diffapp_max" [] e_metID

   128  (["DiffApp","max_by_calculus"]:metID,

   129   [("#Given" ,["fixedValues fix_","maximum m_","relations rs_",

   130 	       "boundVariable v_","interval itv_","errorBound err_"]),

   131     ("#Find"  ,["valuesFor vs_"]),

   132     ("#Relate",[])

   133     ],

   134   {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,

   135     crls = eval_rls, nrls=norm_Rational

   136    (*,  asm_rls=[],asm_thm=[]*)},

   137   "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\

   138    \      (v_::real) (itv_::real set) (err_::bool) =          \ 

   139    \ (let e_ = (hd o (filterVar m_)) rs_;              \

   140    \      t_ = (if 1 < length_ rs_                            \

   141    \           then (SubProblem (DiffApp_,[make,function],[no_met])\

   142    \                     [real_ m_, real_ v_, bool_list_ rs_])\

   143    \           else (hd rs_));                                \

   144    \      (mx_::real) = SubProblem(DiffApp_,[on_interval,maximum_of,function],\

   145    \                                [DiffApp,max_on_interval_by_calculus])\

   146    \                               [bool_ t_, real_ v_, real_set_ itv_]\

   147    \ in ((SubProblem (DiffApp_,[find_values,tool],[Isac,find_values])   \

   148    \      [real_ mx_, real_ (Rhs t_), real_ v_, real_ m_,     \

   149    \       bool_list_ (dropWhile (ident e_) rs_)])::bool list))"

   150   ));

   151 store_met

   152  (prep_met DiffApp.thy "met_diffapp_funnew" [] e_metID

   153  (["DiffApp","make_fun_by_new_variable"]:metID,

   154    [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),

   155     ("#Find"  ,["functionEq f_1_"])

   156     ],

   157    {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls,

   158     calc=[], crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)},

   159   "Script Make_fun_by_new_variable (f_::real) (v_::real)     \

   160    \      (eqs_::bool list) =                                 \

   161    \(let h_ = (hd o (filterVar f_)) eqs_;             \

   162    \     es_ = dropWhile (ident h_) eqs_;                    \

   163    \     vs_ = dropWhile (ident f_) (Vars h_);                \

   164    \     v_1 = nth_ 1 vs_;                                   \

   165    \     v_2 = nth_ 2 vs_;                                   \

   166    \     e_1 = (hd o (filterVar v_1)) es_;            \

   167    \     e_2 = (hd o (filterVar v_2)) es_;            \

   168    \  (s_1::bool list) = (SubProblem (DiffApp_,[univariate,equation],[no_met])\

   169    \                    [bool_ e_1, real_ v_1]);\

   170    \  (s_2::bool list) = (SubProblem (DiffApp_,[univariate,equation],[no_met])\

   171    \                    [bool_ e_2, real_ v_2])\

   172    \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)"

   173 ));

   174 store_met

   175 (prep_met DiffApp.thy "met_diffapp_funexp" [] e_metID

   176 (["DiffApp","make_fun_by_explicit"]:metID,

   177    [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),

   178     ("#Find"  ,["functionEq f_1_"])

   179     ],

   180    {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,

   181     crls = eval_rls, nrls=norm_Rational

   182     (*, asm_rls=[],asm_thm=[]*)},

   183    "Script Make_fun_by_explicit (f_::real) (v_::real)         \

   184    \      (eqs_::bool list) =                                 \

   185    \ (let h_ = (hd o (filterVar f_)) eqs_;                    \

   186    \      e_1 = hd (dropWhile (ident h_) eqs_);       \

   187    \      vs_ = dropWhile (ident f_) (Vars h_);                \

   188    \      v_1 = hd (dropWhile (ident v_) vs_);                \

   189    \      (s_1::bool list)=(SubProblem(DiffApp_,[univariate,equation],[no_met])\

   190    \                          [bool_ e_1, real_ v_1])\

   191    \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)"

   192    ));

   193 store_met

   194  (prep_met DiffApp.thy "met_diffapp_max_oninterval" [] e_metID

   195  (["DiffApp","max_on_interval_by_calculus"]:metID,

   196    [("#Given" ,["functionEq t_","boundVariable v_","interval itv_"(*,

   197 		"errorBound err_"*)]),

   198     ("#Find"  ,["maxArgument v_0_"])

   199     ],

   200    {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,

   201     crls = eval_rls, nrls=norm_Rational

   202     (*, asm_rls=[],asm_thm=[]*)},

   203    "empty_script"

   204    ));

   205 store_met

   206  (prep_met DiffApp.thy "met_diffapp_findvals" [] e_metID

   207  (["DiffApp","find_values"]:metID,

   208    [],

   209    {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,

   210     crls = eval_rls, nrls=norm_Rational(*,

   211     asm_rls=[],asm_thm=[]*)},

   212    "empty_script"));

   213 

   214 val list_rls = append_rls "list_rls" list_rls

   215 			  [Thm ("filterVar_Const", num_str filterVar_Const),

   216 			   Thm ("filterVar_Nil", num_str filterVar_Nil)

   217 			   ];

   218 ruleset' := overwritelthy thy (!ruleset',

   219   [("list_rls",list_rls)

   220    ]);

   221
wneuper/isa