(* application of differential calculus

   Walther Neuper 2002

   (c) due to copyright terms

*)

theory DiffApp imports Diff begin

consts

  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 \<open>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.    

\<close>

ML \<open>

val thy = @{theory};

val eval_rls = prep_rls' (

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

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

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

      Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),

      Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),

      Rule.Thm ("not_true", TermC.num_str @{thm not_true}),

      Rule.Thm ("not_false", TermC.num_str @{thm not_false}),

      Rule.Thm ("and_true", TermC.num_str @{thm and_true}),

      Rule.Thm ("and_false", TermC.num_str @{thm and_false}),

      Rule.Thm ("or_true", TermC.num_str @{thm or_true}),

      Rule.Thm ("or_false", TermC.num_str @{thm or_false}),

      Rule.Thm ("and_commute", TermC.num_str @{thm and_commute}),

      Rule.Thm ("or_commute", TermC.num_str @{thm or_commute}),

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

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

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

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

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

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

    scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

    });

\<close>

setup \<open>KEStore_Elems.add_rlss [("eval_rls", (Context.theory_name @{theory}, eval_rls))]\<close>

(** problem types **)

setup \<open>KEStore_Elems.add_pbts

  [(Specify.prep_pbt thy "pbl_fun_max" [] Celem.e_pblID

      (["maximum_of","function"],

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

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

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

        Rule.e_rls, NONE, [])),

    (Specify.prep_pbt thy "pbl_fun_make" [] Celem.e_pblID

      (["make","function"],

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

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

        Rule.e_rls, NONE, [])),

    (Specify.prep_pbt thy "pbl_fun_max_expl" [] Celem.e_pblID

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

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

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

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

    (Specify.prep_pbt thy "pbl_fun_max_newvar" [] Celem.e_pblID

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

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

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

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

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

    (Specify.prep_pbt thy "pbl_fun_max_interv" [] Celem.e_pblID

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

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

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

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

      Rule.e_rls, NONE, [])),

    (Specify.prep_pbt thy "pbl_tool" [] Celem.e_pblID

      (["tool"], [], Rule.e_rls, NONE, [])),

    (Specify.prep_pbt thy "pbl_tool_findvals" [] Celem.e_pblID

      (["find_values","tool"],

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

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

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

      Rule.e_rls, NONE, []))]\<close>

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

setup \<open>KEStore_Elems.add_mets

    [Specify.prep_met thy "met_diffapp" [] Celem.e_metID

      (["DiffApp"], [],

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

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

        @{thm refl})]

\<close>

partial_function (tailrec) maximum_value ::

  "bool list \<Rightarrow> real \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> real set \<Rightarrow> bool \<Rightarrow> bool list"

  where

"maximum_value f_ix m_m r_s v_v itv_v e_rr =

 (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 = SubProblem (''DiffApp'', [''on_interval'', ''maximum_of'', ''function''],

                [''DiffApp'', ''max_on_interval_by_calculus''])

              [BOOL t_t, REAL v_v, REAL_SET itv_v]

 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)])"

setup \<open>KEStore_Elems.add_mets

    [Specify.prep_met thy "met_diffapp_max" [] Celem.e_metID

      (["DiffApp","max_by_calculus"],

        [("#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=Rule.e_rls, crls = eval_rls,

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

      @{thm maximum_value.simps})]

\<close>

partial_function (tailrec) make_fun_by_new_variable :: "real => real => bool list => bool"

  where

"make_fun_by_new_variable f_f v_v eqs =

  (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 = SubProblem (''DiffApp'', [''univariate'', ''equation''], [''no_met''])

                [BOOL e_1, REAL v_1];

       s_2 = 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)"

setup \<open>KEStore_Elems.add_mets

    [Specify.prep_met thy "met_diffapp_funnew" [] Celem.e_metID

      (["DiffApp","make_fun_by_new_variable"],

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

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

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

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

        @{thm make_fun_by_new_variable.simps})]

\<close>

partial_function (tailrec) make_fun_by_explicit :: "real => real => bool list => bool"

  where

"make_fun_by_explicit f_f v_v eqs =                                          

 (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 = SubProblem(''DiffApp'', [''univariate'', ''equation''], [''no_met''])

              [BOOL e_1, REAL v_1]

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

setup \<open>KEStore_Elems.add_mets

    [Specify.prep_met thy "met_diffapp_funexp" [] Celem.e_metID

      (["DiffApp","make_fun_by_explicit"],

        [("#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=Rule.e_rls, crls = eval_rls,

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

        @{thm make_fun_by_explicit.simps})]

\<close>

setup \<open>KEStore_Elems.add_mets

    [Specify.prep_met thy "met_diffapp_max_oninterval" [] Celem.e_metID

      (["DiffApp","max_on_interval_by_calculus"],

        [("#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 = Rule.e_rls,prls=Rule.e_rls, crls = eval_rls,

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

      @{thm refl}),

    Specify.prep_met thy "met_diffapp_findvals" [] Celem.e_metID

      (["DiffApp","find_values"], [],

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

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

        @{thm refl})]

\<close>

ML \<open>

val list_rls = Rule.append_rls "list_rls" list_rls

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

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

\<close>

setup \<open>KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))]\<close>

end