(* application of differential calculus

   Walther Neuper 2002

   (c) due to copyright terms

*)

theory DiffApp imports Diff begin

consts

  dummy :: real

fun filterVar :: \<open>real \<Rightarrow> 'a  list \<Rightarrow> 'a  list\<close>

  where

    filterVar_Nil: \<open>filterVar v [] = []\<close>

  | filterVar_Const: \<open>filterVar v (x # xs) =

      (if v \<in> set (Vars x) then x # (filterVar v xs) else filterVar v xs)\<close>

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 (Input_Descript.thy)

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

- mk_arg, arguments_from_model ... 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, arguments_from_model just make most convenient env

  from penv as is.    

\<close>

ML \<open>

val eval_rls = prep_rls' (

  Rule_Def.Repeat {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI), 

    erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],

    rules = [

      \<^rule_thm>\<open>refl\<close>,

      \<^rule_thm>\<open>order_refl\<close>,

      \<^rule_thm>\<open>radd_left_cancel_le\<close>,

      \<^rule_thm>\<open>not_true\<close>,

      \<^rule_thm>\<open>not_false\<close>,

      \<^rule_thm>\<open>and_true\<close>,

      \<^rule_thm>\<open>and_false\<close>,

      \<^rule_thm>\<open>or_true\<close>,

      \<^rule_thm>\<open>or_false\<close>,

      \<^rule_thm>\<open>and_commute\<close>,

      \<^rule_thm>\<open>or_commute\<close>,

      \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),

      \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),

      \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),    

    	\<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),

      \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),    

      \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")],

    scr = Rule.Empty_Prog

    });

\<close>

rule_set_knowledge eval_rls = \<open>eval_rls\<close>

(** problems **)

problem pbl_fun_max : "maximum_of/function" =

  \<open>Rule_Set.empty\<close>

  Given: "fixedValues f_ix"

  Find: "maximum m_m" "valuesFor v_s"

  Relate: "relations r_s"

problem pbl_fun_make : "make/function" =

  \<open>Rule_Set.empty\<close>

  Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"

  Find: "functionEq f_1"

problem pbl_fun_max_expl : "by_explicit/make/function" =

  \<open>Rule_Set.empty\<close>

  Method_Ref: "DiffApp/make_fun_by_explicit"

  Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"

  Find: "functionEq f_1"

problem pbl_fun_max_newvar : "by_new_variable/make/function" =

  \<open>Rule_Set.empty\<close>

  Method_Ref: "DiffApp/make_fun_by_new_variable"

  Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"

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

  Find: "functionEq f_1"

problem pbl_fun_max_interv : "on_interval/maximum_of/function" =

  \<open>Rule_Set.empty\<close>

  Given: "functionEq t_t" "boundVariable v_v" "interval i_tv"

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

  Find: "maxArgument v_0"

problem  pbl_tool : "tool" =

  \<open>Rule_Set.empty\<close>

problem pbl_tool_findvals : "find_values/tool" =

  \<open>Rule_Set.empty\<close>

  Given: "maxArgument m_ax" "functionEq f_f" "boundVariable v_v"

  Find: "valuesFor v_ls"

  Relate: "additionalRels r_s"

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

method met_diffapp : "DiffApp" =

  \<open>{rew_ord'="tless_true", rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,

    crls = Atools_erls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}\<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_Knowledge'', ''find_values''])

      [REAL m_x, REAL (rhs t_t), REAL v_v, REAL m_m, BOOL_LIST (dropWhile (ident e_e) r_s)])"

method met_diffapp_max : "DiffApp/max_by_calculus" =

  \<open>{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=prog_expr,prls=Rule_Set.empty, crls = eval_rls,

    errpats = [], nrls = norm_Rational (*,  asm_rls=[],asm_thm=[]*)}\<close>

  Program: maximum_value.simps

  Given: "fixedValues f_ix" "maximum m_m" "relations r_s" "boundVariable v_v"

    "interval i_tv" "errorBound e_rr"

  Find: "valuesFor v_s"

  Relate:

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

method met_diffapp_funnew : "DiffApp/make_fun_by_new_variable" =

  \<open>{rew_ord'="tless_true",rls'=eval_rls,srls=prog_expr,prls=Rule_Set.empty, calc=[], crls = eval_rls,

          errpats = [], nrls = norm_Rational(*,asm_rls=[],asm_thm=[]*)}\<close>

  Program: make_fun_by_new_variable.simps

  Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"

  Find: "functionEq f_1"

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

method met_diffapp_funexp : "DiffApp/make_fun_by_explicit" =

  \<open>{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=prog_expr,prls=Rule_Set.empty, crls = eval_rls,

    errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}\<close>

  Program: make_fun_by_explicit.simps

  Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"

  Find: "functionEq f_1"

method met_diffapp_max_oninterval : "DiffApp/max_on_interval_by_calculus" =

  \<open>{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,

    errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}\<close>

  Given: "functionEq t_t" "boundVariable v_v" "interval i_tv" (*"errorBound e_rr"*)

  Find: "maxArgument v_0"

method met_diffapp_findvals : "DiffApp/find_values" =

  \<open>{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,

    errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)}\<close>

ML \<open>

\<close> ML \<open>

val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [

   \<^rule_thm>\<open>filterVar_Const\<close>,

   \<^rule_thm>\<open>filterVar_Nil\<close>];

\<close>

rule_set_knowledge prog_expr = \<open>prog_expr\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

end