1 (* application of differential calculus
3 (c) due to copyright terms
6 theory Diff_App imports Diff begin
12 fun filterVar :: \<open>real \<Rightarrow> 'a list \<Rightarrow> 'a list\<close>
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>
20 val eval_rls = prep_rls' (
21 Rule_Def.Repeat {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI),
22 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
24 \<^rule_thm>\<open>refl\<close>,
25 \<^rule_thm>\<open>order_refl\<close>,
26 \<^rule_thm>\<open>radd_left_cancel_le\<close>,
27 \<^rule_thm>\<open>not_true\<close>,
28 \<^rule_thm>\<open>not_false\<close>,
29 \<^rule_thm>\<open>and_true\<close>,
30 \<^rule_thm>\<open>and_false\<close>,
31 \<^rule_thm>\<open>or_true\<close>,
32 \<^rule_thm>\<open>or_false\<close>,
33 \<^rule_thm>\<open>and_commute\<close>,
34 \<^rule_thm>\<open>or_commute\<close>,
36 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
37 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
39 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
40 \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
41 \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
42 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")],
43 program = Rule.Empty_Prog
46 rule_set_knowledge eval_rls = \<open>eval_rls\<close>
50 problem pbl_fun_max : "maximum_of/function" =
51 \<open>Rule_Set.empty\<close>
52 Given: "fixedValues f_ix"
53 Find: "maximum m_m" "valuesFor v_s"
54 Relate: "relations r_s"
56 problem pbl_fun_make : "make/function" =
57 \<open>Rule_Set.empty\<close>
58 Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
59 Find: "functionEq f_1"
61 problem pbl_fun_max_expl : "by_explicit/make/function" =
62 \<open>Rule_Set.empty\<close>
63 Method_Ref: "Diff_App/make_fun_by_explicit"
64 Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
65 Find: "functionEq f_1"
67 problem pbl_fun_max_newvar : "by_new_variable/make/function" =
68 \<open>Rule_Set.empty\<close>
69 Method_Ref: "Diff_App/make_fun_by_new_variable"
70 Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
71 (*WN.12.5.03: precond for distinction still missing*)
72 Find: "functionEq f_1"
74 problem pbl_fun_max_interv : "on_interval/maximum_of/function" =
75 \<open>Rule_Set.empty\<close>
76 Given: "functionEq t_t" "boundVariable v_v" "interval i_tv"
77 (*WN.12.5.03: precond for distinction still missing*)
78 Find: "maxArgument v_0"
80 problem pbl_tool : "tool" =
81 \<open>Rule_Set.empty\<close>
83 problem pbl_tool_findvals : "find_values/tool" =
84 \<open>Rule_Set.empty\<close>
85 Given: "maxArgument m_ax" "functionEq f_f" "boundVariable v_v"
86 Find: "valuesFor v_ls"
87 Relate: "additionalRels r_s"
89 problem pbl_opti : "Optimisation" =
90 \<open>Rule_Set.empty\<close>
92 problem pbl_opti_univ : "univariate_calculus/Optimisation" =
93 \<open>eval_rls\<close> (*for evaluation of 0 < r*)
94 Method_Ref: "Optimisation/by_univariate_calculus"
95 Given: "Constants fixes"
97 Find: "Maximum maxx" "AdditionalValues vals"
98 Relate: "Extremum extr" "SideConditions sideconds"
101 (** methods, scripts not yet implemented **)
103 method met_diffapp : "Diff_App" =
104 \<open>{rew_ord="tless_true", rls'=Atools_erls,calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty,
105 errpats = [], rew_rls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}\<close>
107 partial_function (tailrec) maximum_value ::
108 "bool list \<Rightarrow> real \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> real set \<Rightarrow> bool \<Rightarrow> bool list"
110 "maximum_value f_ix m_m r_s v_v itv_v e_rr =
111 (let e_e = (hd o (filterVar m_m)) r_s;
112 t_t = if 1 < Length r_s
113 then SubProblem (''Diff_App'', [''make'', ''function''],[''no_met''])
114 [REAL m_m, REAL v_v, BOOL_LIST r_s]
116 m_x = SubProblem (''Diff_App'', [''on_interval'', ''maximum_of'', ''function''],
117 [''Diff_App'', ''max_on_interval_by_calculus''])
118 [BOOL t_t, REAL v_v, REAL_SET itv_v]
119 in SubProblem (''Diff_App'',[''find_values'', ''tool''], [''Isac_Knowledge'', ''find_values''])
120 [REAL m_x, REAL (rhs t_t), REAL v_v, REAL m_m, BOOL_LIST (dropWhile (ident e_e) r_s)])"
122 method met_diffapp_max : "Diff_App/max_by_calculus" =
123 \<open>{rew_ord="tless_true",rls'=eval_rls,calc=[],prog_rls=prog_expr,where_rls=Rule_Set.empty,
124 errpats = [], rew_rls = norm_Rational}\<close>
125 Program: maximum_value.simps
126 Given: "fixedValues f_ix" "maximum m_m" "relations r_s" "boundVariable v_v"
127 "interval i_tv" "errorBound e_rr"
128 Find: "valuesFor v_s"
131 partial_function (tailrec) make_fun_by_new_variable :: "real => real => bool list => bool"
133 "make_fun_by_new_variable f_f v_v eqs =
134 (let h_h = (hd o (filterVar f_f)) eqs;
135 e_s = dropWhile (ident h_h) eqs;
136 v_s = dropWhile (ident f_f) (Vars h_h);
139 e_1 = (hd o (filterVar v_1)) e_s;
140 e_2 = (hd o (filterVar v_2)) e_s;
141 s_1 = SubProblem (''Diff_App'', [''univariate'', ''equation''], [''no_met''])
142 [BOOL e_1, REAL v_1];
143 s_2 = SubProblem (''Diff_App'', [''univariate'', ''equation''], [''no_met''])
145 in Substitute [(v_1 = (rhs o hd) s_1), (v_2 = (rhs o hd) s_2)] h_h)"
147 method met_diffapp_funnew : "Diff_App/make_fun_by_new_variable" =
148 \<open>{rew_ord="tless_true",rls'=eval_rls,prog_rls=prog_expr,where_rls=Rule_Set.empty, calc=[],
149 errpats = [], rew_rls = norm_Rational(*,asm_rls=[],asm_thm=[]*)}\<close>
150 Program: make_fun_by_new_variable.simps
151 Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
152 Find: "functionEq f_1"
154 partial_function (tailrec) make_fun_by_explicit :: "real => real => bool list => bool"
156 "make_fun_by_explicit f_f v_v eqs =
157 (let h_h = (hd o (filterVar f_f)) eqs;
158 e_1 = hd (dropWhile (ident h_h) eqs);
159 v_s = dropWhile (ident f_f) (Vars h_h);
160 v_1 = hd (dropWhile (ident v_v) v_s);
161 s_1 = SubProblem(''Diff_App'', [''univariate'', ''equation''], [''no_met''])
163 in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "
165 method met_diffapp_funexp : "Diff_App/make_fun_by_explicit" =
166 \<open>{rew_ord="tless_true",rls'=eval_rls,calc=[],prog_rls=prog_expr,where_rls=Rule_Set.empty,
167 errpats = [], rew_rls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}\<close>
168 Program: make_fun_by_explicit.simps
169 Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
170 Find: "functionEq f_1"
172 method met_diffapp_max_oninterval : "Diff_App/max_on_interval_by_calculus" =
173 \<open>{rew_ord="tless_true",rls'=eval_rls,calc=[],prog_rls = Rule_Set.empty,where_rls=Rule_Set.empty,
174 errpats = [], rew_rls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}\<close>
175 Given: "functionEq t_t" "boundVariable v_v" "interval i_tv" (*"errorBound e_rr"*)
176 Find: "maxArgument v_0"
178 method met_diffapp_findvals : "Diff_App/find_values" =
179 \<open>{rew_ord="tless_true",rls'=eval_rls,calc=[],prog_rls = Rule_Set.empty,where_rls=Rule_Set.empty,
180 errpats = [], rew_rls = norm_Rational(*, asm_rls = [], asm_thm = []*)}\<close>
182 method met_opti : "Optimisation" =
183 \<open>{rew_ord = "tless_true", rls' = Atools_erls, calc = [], prog_rls = Rule_Set.empty,
184 where_rls = Rule_Set.empty, errpats = [], rew_rls = norm_Rational}\<close>
186 (*this function has not yet been tested*)
187 partial_function (tailrec) univar_optimisation ::
188 "bool list \<Rightarrow> real \<Rightarrow> bool \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> real set \<Rightarrow> bool \<Rightarrow> bool list"
190 "univar_optimisation fixes maxx extr sideconds funvar doma err =
191 (let e_e = (hd o (filterVar maxx)) sideconds;
192 t_t = if 1 < Length sideconds
193 then SubProblem (''Diff_App'', [''make'', ''function''],[''no_met''])
194 [REAL maxx, REAL funvar, BOOL_LIST sideconds]
196 m_x = SubProblem (''Diff_App'', [''on_interval'', ''maximum_of'', ''function''],
197 [''Diff_App'', ''max_on_interval_by_calculus''])
198 [BOOL t_t, REAL funvar, REAL_SET doma]
199 in SubProblem (''Diff_App'',[''find_values'', ''tool''], [''Isac_Knowledge'', ''find_values''])
200 [REAL m_x, REAL (rhs t_t), REAL funvar, REAL maxx, BOOL_LIST (dropWhile (ident e_e) sideconds)])"
201 (*? return (Maximum, AdditionalValues) ? or only AdditionalValues ?*)
203 method met_opti_univ : "Optimisation/by_univariate_calculus" =
204 \<open>{rew_ord="tless_true",rls'=eval_rls,calc=[],prog_rls=prog_expr,where_rls=Rule_Set.empty,
205 errpats = [], rew_rls = norm_Rational}\<close>
206 Program: univar_optimisation.simps
207 Given: "Constants fixes" "Maximum maxx" "Extremum extr" "SideConditions sideconds"
208 "FunctionVariable funvar" "Domain doma" "ErrorBound err"
209 Find: "AdditionalValues vals"
214 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [
215 \<^rule_thm>\<open>filterVar_Const\<close>,
216 \<^rule_thm>\<open>filterVar_Nil\<close>];
218 rule_set_knowledge prog_expr = \<open>prog_expr\<close>