wneuper/isa: src/Tools/isac/Knowledge/DiffApp.thy@73dc85c025ab

     1 (* application of differential calculus

     2    Walther Neuper 2002

     3    (c) due to copyright terms

     4 *)

     6 theory DiffApp imports Diff begin

     8 consts

    10   Maximum'_value

    11              :: "[bool list,real,bool list,real,real set,bool,

    12 		    bool list] => bool list"

    13                ("((Script Maximum'_value (_ _ _ _ _ _ =))// (_))" 9)

    15   Make'_fun'_by'_new'_variable

    16              :: "[real,real,bool list,

    17 		    bool] => bool"

    18                ("((Script Make'_fun'_by'_new'_variable (_ _ _ =))//

    19 		   (_))" 9)

    20   Make'_fun'_by'_explicit

    21              :: "[real,real,bool list,

    22 		    bool] => bool"

    23                ("((Script Make'_fun'_by'_explicit (_ _ _ =))//

    24 		   (_))" 9)

    26   dummy :: real

    28 (*for script Maximum_value*)

    29   filterVar :: "[real, 'a list] => 'a list"

    31 axiomatization where

    32   filterVar_Nil:		"filterVar v []     = []" and

    33   filterVar_Const:	"filterVar v (x#xs) =

    34 			 (if (v : set (Vars x)) then x#(filterVar v xs)

    35 			                    else filterVar v xs)   "

    36 text {*WN.6.5.03: old decisions in this file partially are being changed

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

    38   Make_fun_by_new_variable, Make_fun_by_explicit.

    39 found to be reconsidered:

    40 - descriptions (Descript.thy)

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

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

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

    44   referencing are labels (no on worksheet))

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

    47   from penv as is.

    48 *}

    50 ML {*

    51 val thy = @{theory};

    53 val eval_rls = prep_rls (

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

    55     erls = e_rls, srls = Erls, calc = [], errpatts = [],

    56     rules = [Thm ("refl", num_str @{thm refl}),

    57       Thm ("order_refl", num_str @{thm order_refl}),

    58       Thm ("radd_left_cancel_le", num_str @{thm radd_left_cancel_le}),

    59       Thm ("not_true", num_str @{thm not_true}),

    60       Thm ("not_false", num_str @{thm not_false}),

    61       Thm ("and_true", num_str @{thm and_true}),

    62       Thm ("and_false", num_str @{thm and_false}),

    63       Thm ("or_true", num_str @{thm or_true}),

    64       Thm ("or_false", num_str @{thm or_false}),

    65       Thm ("and_commute", num_str @{thm and_commute}),

    66       Thm ("or_commute", num_str @{thm or_commute}),

    68       Calc ("Orderings.ord_class.less", eval_equ "#less_"),

    69       Calc ("Orderings.ord_class.less_eq", eval_equ "#less_equal_"),

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

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

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

    74       Calc ("Tools.matches", eval_matches "")],

    75     scr = Prog ((term_of o the o (parse thy)) "empty_script")

    76     }:rls);

    77 *}

    78 setup {* KEStore_Elems.add_rlss [("eval_rls", (Context.theory_name @{theory}, eval_rls))] *}

    79 ML{*

    81 (** problem types **)

    83 store_pbt

    84  (prep_pbt thy "pbl_fun_max" [] e_pblID

    85  (["maximum_of","function"],

    86   [("#Given" ,["fixedValues f_ix"]),

    87    ("#Find"  ,["maximum m_m","valuesFor v_s"]),

    88    ("#Relate",["relations r_s"])

    89   ],

    90   e_rls, NONE, []));

    92 store_pbt

    93  (prep_pbt thy "pbl_fun_make" [] e_pblID

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

    95   [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),

    96    ("#Find"  ,["functionEq f_1"])

    97   ],

    98   e_rls, NONE, []));

    99 store_pbt

   100  (prep_pbt thy "pbl_fun_max_expl" [] e_pblID

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

   102   [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),

   103    ("#Find"  ,["functionEq f_1"])

   104   ],

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

   106 store_pbt

   107  (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID

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

   109   [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),

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

   111    ("#Find"  ,["functionEq f_1"])

   112   ],

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

   115 store_pbt

   116  (prep_pbt thy "pbl_fun_max_interv" [] e_pblID

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

   118   [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"]),

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

   120    ("#Find"  ,["maxArgument v_0"])

   121   ],

   122   e_rls, NONE, []));

   124 store_pbt

   125  (prep_pbt thy "pbl_tool" [] e_pblID

   126  (["tool"]:pblID,

   127   [],

   128   e_rls, NONE, []));

   130 store_pbt

   131  (prep_pbt thy "pbl_tool_findvals" [] e_pblID

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

   133   [("#Given" ,["maxArgument m_ax","functionEq f_f","boundVariable v_v"]),

   134    ("#Find"  ,["valuesFor v_ls"]),

   135    ("#Relate",["additionalRels r_s"])

   136   ],

   137   e_rls, NONE, []));

   138 *}

   139 setup {* KEStore_Elems.add_pbts

   140   [(prep_pbt thy "pbl_fun_max" [] e_pblID

   141       (["maximum_of","function"],

   142         [("#Given" ,["fixedValues f_ix"]),

   143           ("#Find"  ,["maximum m_m","valuesFor v_s"]),

   144           ("#Relate",["relations r_s"])],

   145         e_rls, NONE, [])),

   146     (prep_pbt thy "pbl_fun_make" [] e_pblID

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

   148         [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),

   149           ("#Find"  ,["functionEq f_1"])],

   150         e_rls, NONE, [])),

   151     (prep_pbt thy "pbl_fun_max_expl" [] e_pblID

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

   153         [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),

   154           ("#Find"  ,["functionEq f_1"])],

   155       e_rls, NONE, [["DiffApp","make_fun_by_explicit"]])),

   156     (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID

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

   158         [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),

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

   160           ("#Find"  ,["functionEq f_1"])],

   161       e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]])),

   162     (prep_pbt thy "pbl_fun_max_interv" [] e_pblID

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

   164         [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"]),

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

   166           ("#Find"  ,["maxArgument v_0"])],

   167       e_rls, NONE, [])),

   168     (prep_pbt thy "pbl_tool" [] e_pblID

   169       (["tool"]:pblID, [], e_rls, NONE, [])),

   170     (prep_pbt thy "pbl_tool_findvals" [] e_pblID

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

   172         [("#Given" ,["maxArgument m_ax","functionEq f_f","boundVariable v_v"]),

   173           ("#Find"  ,["valuesFor v_ls"]),

   174           ("#Relate",["additionalRels r_s"])],

   175       e_rls, NONE, []))] *}

   176 ML{*

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

   180 store_met

   181  (prep_met thy "met_diffapp" [] e_metID

   182  (["DiffApp"],

   183    [],

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

   185     crls = Atools_erls, errpats = [], nrls = norm_Rational

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

   187 *}

   188 ML{*

   189 store_met

   190  (prep_met thy "met_diffapp_max" [] e_metID

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

   192   [("#Given" ,["fixedValues f_ix","maximum m_m","relations r_s",

   193 	       "boundVariable v_v","interval i_tv","errorBound e_rr"]),

   194     ("#Find"  ,["valuesFor v_s"]),

   195     ("#Relate",[])

   196     ],

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

   198     crls = eval_rls, errpats = [], nrls = norm_Rational

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

   200   "Script Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list)       " ^

   201   "      (v_v::real) (itv_v::real set) (e_rr::bool) =                       " ^

   202   " (let e_e = (hd o (filterVar m_m)) r_s;                                  " ^

   203   "      t_t = (if 1 < LENGTH r_s                                         " ^

   204   "           then (SubProblem (DiffApp',[make,function],[no_met])        " ^

   205   "                     [REAL m_m, REAL v_v, BOOL_LIST r_s])             " ^

   206   "           else (hd r_s));                                             " ^

   207   "      (m_x::real) =                                                    " ^

   208   "SubProblem(DiffApp',[on_interval,maximum_of,function],                 " ^

   209   "                                [DiffApp,max_on_interval_by_calculus]) " ^

   210   "                               [BOOL t_t, REAL v_v, REAL_SET i_tv]    " ^

   211   " in ((SubProblem (DiffApp',[find_values,tool],[Isac,find_values])      " ^

   212   "      [REAL m_x, REAL (Rhs t_t), REAL v_v, REAL m_m,                  " ^

   213   "       BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list))            "

   214  ));

   215 *}

   216 ML{*

   217 store_met

   218  (prep_met thy "met_diffapp_funnew" [] e_metID

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

   220    [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),

   221     ("#Find"  ,["functionEq f_1"])

   222     ],

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

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

   225   "Script Make_fun_by_new_variable (f_f::real) (v_v::real)                " ^

   226   "      (eqs::bool list) =                                            " ^

   227   "(let h_h = (hd o (filterVar f_f)) eqs;                                " ^

   228   "     e_s = dropWhile (ident h_h) eqs;                                " ^

   229   "     v_s = dropWhile (ident f_f) (Vars h_h);                           " ^

   230   "     v_1 = NTH 1 v_s;                                               " ^

   231   "     v_2 = NTH 2 v_s;                                               " ^

   232   "     e_1 = (hd o (filterVar v_1)) e_s;                               " ^

   233   "     e_2 = (hd o (filterVar v_2)) e_s;                               " ^

   234   "  (s_1::bool list) =                                                 " ^

   235   "                (SubProblem (DiffApp',[univariate,equation],[no_met])" ^

   236   "                    [BOOL e_1, REAL v_1]);                         " ^

   237   "  (s_2::bool list) =                                                 " ^

   238   "                (SubProblem (DiffApp',[univariate,equation],[no_met])" ^

   239   "                    [BOOL e_2, REAL v_2])" ^

   240   "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)"

   241 ));

   242 *}

   243 ML{*

   244 store_met

   245 (prep_met thy "met_diffapp_funexp" [] e_metID

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

   247    [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),

   248     ("#Find"  ,["functionEq f_1"])

   249     ],

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

   251     crls = eval_rls, errpats = [], nrls = norm_Rational

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

   253    "Script Make_fun_by_explicit (f_f::real) (v_v::real)                 " ^

   254    "      (eqs::bool list) =                                         " ^

   255    " (let h_h = (hd o (filterVar f_f)) eqs;                            " ^

   256    "      e_1 = hd (dropWhile (ident h_h) eqs);                       " ^

   257    "      v_s = dropWhile (ident f_f) (Vars h_h);                       " ^

   258    "      v_1 = hd (dropWhile (ident v_v) v_s);                        " ^

   259    "      (s_1::bool list)=                                           " ^

   260    "              (SubProblem(DiffApp',[univariate,equation],[no_met])" ^

   261    "                          [BOOL e_1, REAL v_1])                 " ^

   262    " in Substitute [(v_1 = (rhs o hd) s_1)] h_h)                       "

   263    ));

   264 *}

   265 ML{*

   266 store_met

   267  (prep_met thy "met_diffapp_max_oninterval" [] e_metID

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

   269    [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"(*,

   270 		"errorBound e_rr"*)]),

   271     ("#Find"  ,["maxArgument v_0"])

   272     ],

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

   274     crls = eval_rls, errpats = [], nrls = norm_Rational

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

   276    "empty_script"

   277    ));

   278 *}

   279 ML{*

   280 store_met

   281  (prep_met thy "met_diffapp_findvals" [] e_metID

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

   283    [],

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

   285     crls = eval_rls, errpats = [], nrls = norm_Rational(*,

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

   287    "empty_script"));

   289 val list_rls = append_rls "list_rls" list_rls

   290   [Thm ("filterVar_Const", num_str @{thm filterVar_Const}),

   291    Thm ("filterVar_Nil", num_str @{thm filterVar_Nil})];

   292 *}

   293 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}

   295 end

author	Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
	Mon, 27 Jan 2014 21:49:27 +0100
changeset 55359	73dc85c025ab
parent 55339	cccd24e959ba
child 55363	d78bc1342183
permissions	-rw-r--r--