wneuper/isa: src/Tools/isac/Knowledge/DiffApp.thy@d3a3cc2f0382

     1 (* application of differential calculus

     2    Walther Neuper 2002

     3    (c) due to copyright terms

     4 *)

     6 theory DiffApp imports Diff begin

     8 consts

    10   dummy :: real

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

    13   where

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

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

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

    19 text \<open>WN.6.5.03: old decisions in this file partially are being changed

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

    21   Make_fun_by_new_variable, Make_fun_by_explicit.

    22 found to be reconsidered:

    23 - descriptions (Input_Descript.thy)

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

    25 - mk_arg, arguments_from_model ... env in script different from penv ?

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

    27   referencing are labels (no on worksheet))

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

    30   from penv as is.

    31 \<close>

    33 ML \<open>

    34 val eval_rls = prep_rls' (

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

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

    37     rules = [

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    57     scr = Rule.Empty_Prog

    58     });

    59 \<close>

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

    62 (** problems **)

    64 problem pbl_fun_max : "maximum_of/function" =

    65   \<open>Rule_Set.empty\<close>

    66   Given: "fixedValues f_ix"

    67   Find: "maximum m_m" "valuesFor v_s"

    68   Relate: "relations r_s"

    70 problem pbl_fun_make : "make/function" =

    71   \<open>Rule_Set.empty\<close>

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

    73   Find: "functionEq f_1"

    75 problem pbl_fun_max_expl : "by_explicit/make/function" =

    76   \<open>Rule_Set.empty\<close>

    77   Method: "DiffApp/make_fun_by_explicit"

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

    79   Find: "functionEq f_1"

    81 problem pbl_fun_max_newvar : "by_new_variable/make/function" =

    82   \<open>Rule_Set.empty\<close>

    83   Method: "DiffApp/make_fun_by_new_variable"

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

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

    86   Find: "functionEq f_1"

    88 problem pbl_fun_max_interv : "on_interval/maximum_of/function" =

    89   \<open>Rule_Set.empty\<close>

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

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

    92   Find: "maxArgument v_0"

    94 problem  pbl_tool : "tool" =

    95   \<open>Rule_Set.empty\<close>

    97 problem pbl_tool_findvals : "find_values/tool" =

    98   \<open>Rule_Set.empty\<close>

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

   100   Find: "valuesFor v_ls"

   101   Relate: "additionalRels r_s"

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

   106 method met_diffapp : "DiffApp" =

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

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

   110 partial_function (tailrec) maximum_value ::

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

   112   where

   113 "maximum_value f_ix m_m r_s v_v itv_v e_rr =

   114  (let e_e = (hd o (filterVar m_m)) r_s;

   115       t_t = if 1 < Length r_s

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

   117                    [REAL m_m, REAL v_v, BOOL_LIST r_s]

   118             else (hd r_s);

   119       m_x = SubProblem (''DiffApp'', [''on_interval'', ''maximum_of'', ''function''],

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

   121               [BOOL t_t, REAL v_v, REAL_SET itv_v]

   122  in SubProblem (''DiffApp'',[''find_values'', ''tool''], [''Isac_Knowledge'', ''find_values''])

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

   125 method met_diffapp_max : "DiffApp/max_by_calculus" =

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

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

   128   Program: maximum_value.simps

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

   130     "interval i_tv" "errorBound e_rr"

   131   Find: "valuesFor v_s"

   132   Relate:

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

   135   where

   136 "make_fun_by_new_variable f_f v_v eqs =

   137   (let h_h = (hd o (filterVar f_f)) eqs;

   138        e_s = dropWhile (ident h_h) eqs;

   139        v_s = dropWhile (ident f_f) (Vars h_h);

   140        v_1 = NTH 1 v_s;

   141        v_2 = NTH 2 v_s;

   142        e_1 = (hd o (filterVar v_1)) e_s;

   143        e_2 = (hd o (filterVar v_2)) e_s;

   144        s_1 = SubProblem (''DiffApp'', [''univariate'', ''equation''], [''no_met''])

   145                 [BOOL e_1, REAL v_1];

   146        s_2 = SubProblem (''DiffApp'', [''univariate'', ''equation''], [''no_met''])

   147                 [BOOL e_2, REAL v_2]

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

   150 method met_diffapp_funnew : "DiffApp/make_fun_by_new_variable" =

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

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

   153   Program: make_fun_by_new_variable.simps

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

   155   Find: "functionEq f_1"

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

   158   where

   159 "make_fun_by_explicit f_f v_v eqs =

   160  (let h_h = (hd o (filterVar f_f)) eqs;

   161       e_1 = hd (dropWhile (ident h_h) eqs);

   162       v_s = dropWhile (ident f_f) (Vars h_h);

   163       v_1 = hd (dropWhile (ident v_v) v_s);

   164       s_1 = SubProblem(''DiffApp'', [''univariate'', ''equation''], [''no_met''])

   165               [BOOL e_1, REAL v_1]

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

   168 method met_diffapp_funexp : "DiffApp/make_fun_by_explicit" =

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

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

   171   Program: make_fun_by_explicit.simps

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

   173   Find: "functionEq f_1"

   175 method met_diffapp_max_oninterval : "DiffApp/max_on_interval_by_calculus" =

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

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

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

   179   Find: "maxArgument v_0"

   181 method met_diffapp_findvals : "DiffApp/find_values" =

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

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

   185 ML \<open>

   186 \<close> ML \<open>

   187 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [

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

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

   190 \<close>

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

   192 ML \<open>

   193 \<close> ML \<open>

   194 \<close> ML \<open>

   195 \<close>

   196 end

author	wneuper <walther.neuper@jku.at>
	Wed, 18 Aug 2021 16:03:08 +0200
changeset 60385	d3a3cc2f0382
parent 60380	ab55837e42c4
child 60449	2406d378cede
permissions	-rw-r--r--