(* tools for applications of differetiation

 use"DiffApp.ML";

 use"Knowledge/DiffApp.ML";

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

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.    

 *)

(** interface isabelle -- isac **)

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

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

		Thm ("le_refl",num_str le_refl),

		Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),

		Thm ("not_true",num_str not_true),

		Thm ("not_false",num_str not_false),

		Thm ("and_true",and_true),

		Thm ("and_false",and_false),

		Thm ("or_true",or_true),

		Thm ("or_false",or_false),

		Thm ("and_commute",num_str and_commute),

		Thm ("or_commute",num_str 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 thy

		(!ruleset',

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

		  ]);

(** problem types **)

store_pbt

 (prep_pbt DiffApp.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 DiffApp.thy "pbl_fun_make" [] e_pblID

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

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

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

  ],

  e_rls, NONE, []));

store_pbt

 (prep_pbt DiffApp.thy "pbl_fun_max_expl" [] e_pblID

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

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

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

  ],

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

store_pbt

 (prep_pbt DiffApp.thy "pbl_fun_max_newvar" [] e_pblID

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

  [("#Given" ,["functionOf f_","boundVariable 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 DiffApp.thy "pbl_fun_max_interv" [] e_pblID

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

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

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

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

  ],

  e_rls, NONE, []));

store_pbt

 (prep_pbt DiffApp.thy "pbl_tool" [] e_pblID

 (["tool"]:pblID,

  [],

  e_rls, NONE, []));

store_pbt

 (prep_pbt DiffApp.thy "pbl_tool_findvals" [] e_pblID

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

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

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

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

  ],

  e_rls, NONE, []));

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

store_met

 (prep_met Diff.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 DiffApp.thy "met_diffapp_max" [] e_metID

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

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

	       "boundVariable 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_::real) (itv_::real set) (err_::bool) =          \ 

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

   \      t_ = (if 1 < length_ rs_                            \

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

   \                     [real_ m_, real_ 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_, real_set_ itv_]\

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

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

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

  ));

store_met

 (prep_met DiffApp.thy "met_diffapp_funnew" [] e_metID

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

   [("#Given" ,["functionOf f_","boundVariable 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_::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 DiffApp.thy "met_diffapp_funexp" [] e_metID

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

   [("#Given" ,["functionOf f_","boundVariable 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_::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_) 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 DiffApp.thy "met_diffapp_max_oninterval" [] e_metID

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

   [("#Given" ,["functionEq t_","boundVariable 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 DiffApp.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 filterVar_Const),

			   Thm ("filterVar_Nil", num_str filterVar_Nil)

			   ];

ruleset' := overwritelthy thy (!ruleset',

  [("list_rls",list_rls)

   ]);