(* application of differential calculus

   Walther Neuper 2002

   (c) due to copyright terms

*)

theory DiffApp imports Diff begin

consts

  Maximum'_value

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

		    bool list] => bool list"

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

  Make'_fun'_by'_new'_variable

             :: "[real,real,bool list,  

		    bool] => bool"

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

		   (_))" 9)

  Make'_fun'_by'_explicit

             :: "[real,real,bool list,  

		    bool] => bool"

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

		   (_))" 9)

  dummy :: real

(*for script Maximum_value*)

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

axiomatization where

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

  filterVar_Const:	"filterVar v (x#xs) =                       

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

			                    else filterVar v xs)   "

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

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

  Make_fun_by_new_variable, Make_fun_by_explicit.

found to be reconsidered:

- descriptions (Descript.thy)

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

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

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

  referencing are labels (no on worksheet))

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

  from penv as is.    

*}

ML {*

val thy = @{theory};

val eval_rls = prep_rls (

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    }:rls);

*}

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

ML{*

(** problem types **)

store_pbt

 (prep_pbt thy "pbl_fun_max" [] e_pblID

 (["maximum_of","function"],

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

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

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

  ],

  e_rls, NONE, []));

store_pbt

 (prep_pbt thy "pbl_fun_make" [] e_pblID

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

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

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

  ],

  e_rls, NONE, []));

store_pbt

 (prep_pbt thy "pbl_fun_max_expl" [] e_pblID

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

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

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

  ],

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

store_pbt

 (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID

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

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

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

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

  ],

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

store_pbt

 (prep_pbt thy "pbl_fun_max_interv" [] e_pblID

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

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

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

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

  ],

  e_rls, NONE, []));

store_pbt

 (prep_pbt thy "pbl_tool" [] e_pblID

 (["tool"]:pblID,

  [],

  e_rls, NONE, []));

store_pbt

 (prep_pbt thy "pbl_tool_findvals" [] e_pblID

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

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

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

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

  ],

  e_rls, NONE, []));

*}

setup {* KEStore_Elems.add_pbts

  [(prep_pbt thy "pbl_fun_max" [] e_pblID

      (["maximum_of","function"],

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

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

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

        e_rls, NONE, [])),

    (prep_pbt thy "pbl_fun_make" [] e_pblID

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

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

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

        e_rls, NONE, [])),

    (prep_pbt thy "pbl_fun_max_expl" [] e_pblID

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

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

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

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

    (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID

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

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

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

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

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

    (prep_pbt thy "pbl_fun_max_interv" [] e_pblID

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

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

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

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

      e_rls, NONE, [])),

    (prep_pbt thy "pbl_tool" [] e_pblID

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

    (prep_pbt thy "pbl_tool_findvals" [] e_pblID

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

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

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

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

      e_rls, NONE, []))] *}

ML{*

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

store_met

 (prep_met thy "met_diffapp" [] e_metID

 (["DiffApp"],

   [],

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

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

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

*}

ML{*

store_met

 (prep_met thy "met_diffapp_max" [] e_metID

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

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

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

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

    ("#Relate",[])

    ],

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

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

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

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

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

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

  "      t_t = (if 1 < LENGTH r_s                                         " ^

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

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

  "           else (hd r_s));                                             " ^

  "      (m_x::real) =                                                    " ^ 

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

  "                                [DiffApp,max_on_interval_by_calculus]) " ^

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

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

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

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

 ));

*}

ML{*

store_met

 (prep_met thy "met_diffapp_funnew" [] e_metID

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

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

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

    ],

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

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

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

  "      (eqs::bool list) =                                            " ^

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

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

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

  "     v_1 = NTH 1 v_s;                                               " ^

  "     v_2 = NTH 2 v_s;                                               " ^

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

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

  "  (s_1::bool list) =                                                 " ^

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

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

  "  (s_2::bool list) =                                                 " ^

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

  "                    [BOOL e_2, REAL v_2])" ^

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

));

*}

ML{*

store_met

(prep_met thy "met_diffapp_funexp" [] e_metID

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

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

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

    ],

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

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

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

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

   "      (eqs::bool list) =                                         " ^

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

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

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

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

   "      (s_1::bool list)=                                           " ^ 

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

   "                          [BOOL e_1, REAL v_1])                 " ^

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

   ));

*}

ML{*

store_met

 (prep_met thy "met_diffapp_max_oninterval" [] e_metID

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

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

		"errorBound e_rr"*)]),

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

    ],

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

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

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

   "empty_script"

   ));

*}

ML{*

store_met

 (prep_met thy "met_diffapp_findvals" [] e_metID

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

   [],

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

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

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

   "empty_script"));

val list_rls = append_rls "list_rls" list_rls

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

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

*}

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

end