(* 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"

(*primrec*)axioms

  filterVar_Nil		"filterVar v []     = []"

  filterVar_Const	"filterVar v (x#xs) =                       

			 (if (v mem (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 = [], (*asm_thm = [],*)

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

		Thm ("real_le_refl",num_str @{thm real_le_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 ("op <",eval_equ "#less_"),

		Calc ("op <=",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 = Script ((term_of o the o (parse thy)) 

      "empty_script")

      }:rls);

ruleset' := overwritelthy @{theory}

		(!ruleset',

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

		  ]);

(** problem types **)

store_pbt

 (prep_pbt thy "pbl_fun_max" [] e_pblID

 (["maximum_of","function"],

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

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

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

  ],

  e_rls, NONE, []));

store_pbt

 (prep_pbt thy "pbl_fun_make" [] e_pblID

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

  [("#Given" ,["functionOf 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_","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_","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_","boundVariable v_v","interval itv_"]),

   (*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 ma_","functionEq f_","boundVariable v_v"]),

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

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

  ],

  e_rls, NONE, []));

(** 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, nrls=norm_Rational

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

store_met

 (prep_met thy "met_diffapp_max" [] e_metID

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

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

	       "boundVariable v_v","interval itv_","errorBound err_"]),

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

    ("#Relate",[])

    ],

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

    crls = eval_rls, nrls=norm_Rational

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

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

  "      (v_v::real) (itv_::real set) (err_::bool) =                       " ^ 

  " (let e_e = (hd o (filterVar m_)) rs_;                                  " ^

  "      t_ = (if 1 < length_ rs_                                         " ^

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

  "                     [real_ m_, real_ v_v, bool_list_ rs_])             " ^

  "           else (hd rs_));                                             " ^

  "      (mx_::real) =                                                    " ^ 

  "SubProblem(DiffApp_,[on_interval,maximum_of,function],                 " ^

  "                                [DiffApp,max_on_interval_by_calculus]) " ^

  "                               [bool_ t_, real_ v_v, real_set_ itv_]    " ^

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

  "      [real_ mx_, real_ (Rhs t_), real_ v_v, real_ m_,                  " ^

  "       bool_list_ (dropWhile (ident e_e) rs_)])::bool list))            "

 ));

store_met

 (prep_met thy "met_diffapp_funnew" [] e_metID

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

   [("#Given" ,["functionOf 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, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)},

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

  "      (eqs_::bool list) =                                            " ^

  "(let h_ = (hd o (filterVar f_)) eqs_;                                " ^

  "     es_ = dropWhile (ident h_) eqs_;                                " ^

  "     vs_ = dropWhile (ident f_) (Vars h_);                           " ^

  "     v_1 = nth_ 1 vs_;                                               " ^

  "     v_2 = nth_ 2 vs_;                                               " ^

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

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

  "  (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_)"

));

store_met

(prep_met thy "met_diffapp_funexp" [] e_metID

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

   [("#Given" ,["functionOf 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, nrls=norm_Rational

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

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

   "      (eqs_::bool list) =                                         " ^

   " (let h_ = (hd o (filterVar f_)) eqs_;                            " ^

   "      e_1 = hd (dropWhile (ident h_) eqs_);                       " ^

   "      vs_ = dropWhile (ident f_) (Vars h_);                       " ^

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

   "      (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_)                       "

   ));

store_met

 (prep_met thy "met_diffapp_max_oninterval" [] e_metID

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

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

		"errorBound err_"*)]),

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

    ],

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

    crls = eval_rls, nrls=norm_Rational

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

   "empty_script"

   ));

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

			   ];

ruleset' := overwritelthy @{theory} (!ruleset',

  [("list_rls",list_rls)

   ]);

*}

end