1 (* application of differential calculus
3 (c) due to copyright terms
6 theory DiffApp imports Diff begin
12 (*for script Maximum_value*)
13 filterVar :: "[real, 'a list] => 'a list"
16 filterVar_Nil: "filterVar v [] = []" and
17 filterVar_Const: "filterVar v (x#xs) =
18 (if (v : set (Vars x)) then x#(filterVar v xs)
19 else filterVar v xs) "
20 text \<open>WN.6.5.03: old decisions in this file partially are being changed
21 in a quick-and-dirty way to make scripts run: Maximum_value,
22 Make_fun_by_new_variable, Make_fun_by_explicit.
23 found to be reconsidered:
24 - descriptions (Input_Descript.thy)
25 - penv: really need term list; or just rerun the whole example with num/var
26 - mk_arg, arguments_from_model ... env in script different from penv ?
27 - L = SubProblem eq ... show some vars on the worksheet ? (other means for
28 referencing are labels (no on worksheet))
30 WN.6.5.03 quick-and-dirty: mk_arg, arguments_from_model just make most convenient env
35 val eval_rls = prep_rls' (
36 Rule_Def.Repeat {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI),
37 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
38 rules = [\<^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_const\<close> (Prog_Expr.eval_const "#is_const_"),
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 "")],
60 rule_set_knowledge eval_rls = \<open>eval_rls\<close>
63 setup \<open>KEStore_Elems.add_pbts
64 [(Problem.prep_input @{theory} "pbl_fun_max" [] Problem.id_empty
65 (["maximum_of", "function"],
66 [("#Given" ,["fixedValues f_ix"]),
67 ("#Find" ,["maximum m_m", "valuesFor v_s"]),
68 ("#Relate",["relations r_s"])],
69 Rule_Set.empty, NONE, [])),
70 (Problem.prep_input @{theory} "pbl_fun_make" [] Problem.id_empty
71 (["make", "function"],
72 [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
73 ("#Find" ,["functionEq f_1"])],
74 Rule_Set.empty, NONE, [])),
75 (Problem.prep_input @{theory} "pbl_fun_max_expl" [] Problem.id_empty
76 (["by_explicit", "make", "function"],
77 [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
78 ("#Find" ,["functionEq f_1"])],
79 Rule_Set.empty, NONE, [["DiffApp", "make_fun_by_explicit"]])),
80 (Problem.prep_input @{theory} "pbl_fun_max_newvar" [] Problem.id_empty
81 (["by_new_variable", "make", "function"],
82 [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
83 (*WN.12.5.03: precond for distinction still missing*)
84 ("#Find" ,["functionEq f_1"])],
85 Rule_Set.empty, NONE, [["DiffApp", "make_fun_by_new_variable"]])),
86 (Problem.prep_input @{theory} "pbl_fun_max_interv" [] Problem.id_empty
87 (["on_interval", "maximum_of", "function"],
88 [("#Given" ,["functionEq t_t", "boundVariable v_v", "interval i_tv"]),
89 (*WN.12.5.03: precond for distinction still missing*)
90 ("#Find" ,["maxArgument v_0"])],
91 Rule_Set.empty, NONE, [])),
92 (Problem.prep_input @{theory} "pbl_tool" [] Problem.id_empty
93 (["tool"], [], Rule_Set.empty, NONE, [])),
94 (Problem.prep_input @{theory} "pbl_tool_findvals" [] Problem.id_empty
95 (["find_values", "tool"],
96 [("#Given" ,["maxArgument m_ax", "functionEq f_f", "boundVariable v_v"]),
97 ("#Find" ,["valuesFor v_ls"]),
98 ("#Relate",["additionalRels r_s"])],
99 Rule_Set.empty, NONE, []))]\<close>
102 (** methods, scripts not yet implemented **)
103 setup \<open>KEStore_Elems.add_mets
104 [MethodC.prep_input @{theory} "met_diffapp" [] MethodC.id_empty
106 {rew_ord'="tless_true", rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
107 crls = Atools_erls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
111 partial_function (tailrec) maximum_value ::
112 "bool list \<Rightarrow> real \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> real set \<Rightarrow> bool \<Rightarrow> bool list"
114 "maximum_value f_ix m_m r_s v_v itv_v e_rr =
115 (let e_e = (hd o (filterVar m_m)) r_s;
116 t_t = if 1 < Length r_s
117 then SubProblem (''DiffApp'', [''make'', ''function''],[''no_met''])
118 [REAL m_m, REAL v_v, BOOL_LIST r_s]
120 m_x = SubProblem (''DiffApp'', [''on_interval'', ''maximum_of'', ''function''],
121 [''DiffApp'', ''max_on_interval_by_calculus''])
122 [BOOL t_t, REAL v_v, REAL_SET itv_v]
123 in SubProblem (''DiffApp'',[''find_values'', ''tool''], [''Isac_Knowledge'', ''find_values''])
124 [REAL m_x, REAL (rhs t_t), REAL v_v, REAL m_m, BOOL_LIST (dropWhile (ident e_e) r_s)])"
125 setup \<open>KEStore_Elems.add_mets
126 [MethodC.prep_input @{theory} "met_diffapp_max" [] MethodC.id_empty
127 (["DiffApp", "max_by_calculus"],
128 [("#Given" ,["fixedValues f_ix", "maximum m_m", "relations r_s", "boundVariable v_v",
129 "interval i_tv", "errorBound e_rr"]),
130 ("#Find" ,["valuesFor v_s"]),
132 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=prog_expr,prls=Rule_Set.empty, crls = eval_rls,
133 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
134 @{thm maximum_value.simps})]
137 partial_function (tailrec) make_fun_by_new_variable :: "real => real => bool list => bool"
139 "make_fun_by_new_variable f_f v_v eqs =
140 (let h_h = (hd o (filterVar f_f)) eqs;
141 e_s = dropWhile (ident h_h) eqs;
142 v_s = dropWhile (ident f_f) (Vars h_h);
145 e_1 = (hd o (filterVar v_1)) e_s;
146 e_2 = (hd o (filterVar v_2)) e_s;
147 s_1 = SubProblem (''DiffApp'', [''univariate'', ''equation''], [''no_met''])
148 [BOOL e_1, REAL v_1];
149 s_2 = SubProblem (''DiffApp'', [''univariate'', ''equation''], [''no_met''])
151 in Substitute [(v_1 = (rhs o hd) s_1), (v_2 = (rhs o hd) s_2)] h_h)"
152 setup \<open>KEStore_Elems.add_mets
153 [MethodC.prep_input @{theory} "met_diffapp_funnew" [] MethodC.id_empty
154 (["DiffApp", "make_fun_by_new_variable"],
155 [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
156 ("#Find" ,["functionEq f_1"])],
157 {rew_ord'="tless_true",rls'=eval_rls,srls=prog_expr,prls=Rule_Set.empty, calc=[], crls = eval_rls,
158 errpats = [], nrls = norm_Rational(*,asm_rls=[],asm_thm=[]*)},
159 @{thm make_fun_by_new_variable.simps})]
162 partial_function (tailrec) make_fun_by_explicit :: "real => real => bool list => bool"
164 "make_fun_by_explicit f_f v_v eqs =
165 (let h_h = (hd o (filterVar f_f)) eqs;
166 e_1 = hd (dropWhile (ident h_h) eqs);
167 v_s = dropWhile (ident f_f) (Vars h_h);
168 v_1 = hd (dropWhile (ident v_v) v_s);
169 s_1 = SubProblem(''DiffApp'', [''univariate'', ''equation''], [''no_met''])
171 in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "
172 setup \<open>KEStore_Elems.add_mets
173 [MethodC.prep_input @{theory} "met_diffapp_funexp" [] MethodC.id_empty
174 (["DiffApp", "make_fun_by_explicit"],
175 [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
176 ("#Find" ,["functionEq f_1"])],
177 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=prog_expr,prls=Rule_Set.empty, crls = eval_rls,
178 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
179 @{thm make_fun_by_explicit.simps})]
181 setup \<open>KEStore_Elems.add_mets
182 [MethodC.prep_input @{theory} "met_diffapp_max_oninterval" [] MethodC.id_empty
183 (["DiffApp", "max_on_interval_by_calculus"],
184 [("#Given" ,["functionEq t_t", "boundVariable v_v", "interval i_tv"(*, "errorBound e_rr"*)]),
185 ("#Find" ,["maxArgument v_0"])],
186 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
187 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
189 MethodC.prep_input @{theory} "met_diffapp_findvals" [] MethodC.id_empty
190 (["DiffApp", "find_values"], [],
191 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
192 errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)},
196 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr
197 [\<^rule_thm>\<open>filterVar_Const\<close>,
198 \<^rule_thm>\<open>filterVar_Nil\<close>];
200 rule_set_knowledge prog_expr = \<open>prog_expr\<close>