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
37 val eval_rls = prep_rls' (
38 Rule_Def.Repeat {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI),
39 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
40 rules = [Rule.Thm ("refl", ThmC.numerals_to_Free @{thm refl}),
41 Rule.Thm ("order_refl", ThmC.numerals_to_Free @{thm order_refl}),
42 Rule.Thm ("radd_left_cancel_le", ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
43 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
44 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
45 Rule.Thm ("and_true", ThmC.numerals_to_Free @{thm and_true}),
46 Rule.Thm ("and_false", ThmC.numerals_to_Free @{thm and_false}),
47 Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
48 Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
49 Rule.Thm ("and_commute", ThmC.numerals_to_Free @{thm and_commute}),
50 Rule.Thm ("or_commute", ThmC.numerals_to_Free @{thm or_commute}),
52 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
53 Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
55 Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
56 Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
57 Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),
58 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")],
62 setup_rule eval_rls = \<open>eval_rls\<close>
65 setup \<open>KEStore_Elems.add_pbts
66 [(Problem.prep_input thy "pbl_fun_max" [] Problem.id_empty
67 (["maximum_of", "function"],
68 [("#Given" ,["fixedValues f_ix"]),
69 ("#Find" ,["maximum m_m", "valuesFor v_s"]),
70 ("#Relate",["relations r_s"])],
71 Rule_Set.empty, NONE, [])),
72 (Problem.prep_input thy "pbl_fun_make" [] Problem.id_empty
73 (["make", "function"],
74 [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
75 ("#Find" ,["functionEq f_1"])],
76 Rule_Set.empty, NONE, [])),
77 (Problem.prep_input thy "pbl_fun_max_expl" [] Problem.id_empty
78 (["by_explicit", "make", "function"],
79 [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
80 ("#Find" ,["functionEq f_1"])],
81 Rule_Set.empty, NONE, [["DiffApp", "make_fun_by_explicit"]])),
82 (Problem.prep_input thy "pbl_fun_max_newvar" [] Problem.id_empty
83 (["by_new_variable", "make", "function"],
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"])],
87 Rule_Set.empty, NONE, [["DiffApp", "make_fun_by_new_variable"]])),
88 (Problem.prep_input thy "pbl_fun_max_interv" [] Problem.id_empty
89 (["on_interval", "maximum_of", "function"],
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"])],
93 Rule_Set.empty, NONE, [])),
94 (Problem.prep_input thy "pbl_tool" [] Problem.id_empty
95 (["tool"], [], Rule_Set.empty, NONE, [])),
96 (Problem.prep_input thy "pbl_tool_findvals" [] Problem.id_empty
97 (["find_values", "tool"],
98 [("#Given" ,["maxArgument m_ax", "functionEq f_f", "boundVariable v_v"]),
99 ("#Find" ,["valuesFor v_ls"]),
100 ("#Relate",["additionalRels r_s"])],
101 Rule_Set.empty, NONE, []))]\<close>
104 (** methods, scripts not yet implemented **)
105 setup \<open>KEStore_Elems.add_mets
106 [MethodC.prep_input thy "met_diffapp" [] MethodC.id_empty
108 {rew_ord'="tless_true", rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
109 crls = Atools_erls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
113 partial_function (tailrec) maximum_value ::
114 "bool list \<Rightarrow> real \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> real set \<Rightarrow> bool \<Rightarrow> bool list"
116 "maximum_value f_ix m_m r_s v_v itv_v e_rr =
117 (let e_e = (hd o (filterVar m_m)) r_s;
118 t_t = if 1 < Length r_s
119 then SubProblem (''DiffApp'', [''make'', ''function''],[''no_met''])
120 [REAL m_m, REAL v_v, BOOL_LIST r_s]
122 m_x = SubProblem (''DiffApp'', [''on_interval'', ''maximum_of'', ''function''],
123 [''DiffApp'', ''max_on_interval_by_calculus''])
124 [BOOL t_t, REAL v_v, REAL_SET itv_v]
125 in SubProblem (''DiffApp'',[''find_values'', ''tool''], [''Isac_Knowledge'', ''find_values''])
126 [REAL m_x, REAL (rhs t_t), REAL v_v, REAL m_m, BOOL_LIST (dropWhile (ident e_e) r_s)])"
127 setup \<open>KEStore_Elems.add_mets
128 [MethodC.prep_input thy "met_diffapp_max" [] MethodC.id_empty
129 (["DiffApp", "max_by_calculus"],
130 [("#Given" ,["fixedValues f_ix", "maximum m_m", "relations r_s", "boundVariable v_v",
131 "interval i_tv", "errorBound e_rr"]),
132 ("#Find" ,["valuesFor v_s"]),
134 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=prog_expr,prls=Rule_Set.empty, crls = eval_rls,
135 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
136 @{thm maximum_value.simps})]
139 partial_function (tailrec) make_fun_by_new_variable :: "real => real => bool list => bool"
141 "make_fun_by_new_variable f_f v_v eqs =
142 (let h_h = (hd o (filterVar f_f)) eqs;
143 e_s = dropWhile (ident h_h) eqs;
144 v_s = dropWhile (ident f_f) (Vars h_h);
147 e_1 = (hd o (filterVar v_1)) e_s;
148 e_2 = (hd o (filterVar v_2)) e_s;
149 s_1 = SubProblem (''DiffApp'', [''univariate'', ''equation''], [''no_met''])
150 [BOOL e_1, REAL v_1];
151 s_2 = SubProblem (''DiffApp'', [''univariate'', ''equation''], [''no_met''])
153 in Substitute [(v_1 = (rhs o hd) s_1), (v_2 = (rhs o hd) s_2)] h_h)"
154 setup \<open>KEStore_Elems.add_mets
155 [MethodC.prep_input thy "met_diffapp_funnew" [] MethodC.id_empty
156 (["DiffApp", "make_fun_by_new_variable"],
157 [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
158 ("#Find" ,["functionEq f_1"])],
159 {rew_ord'="tless_true",rls'=eval_rls,srls=prog_expr,prls=Rule_Set.empty, calc=[], crls = eval_rls,
160 errpats = [], nrls = norm_Rational(*,asm_rls=[],asm_thm=[]*)},
161 @{thm make_fun_by_new_variable.simps})]
164 partial_function (tailrec) make_fun_by_explicit :: "real => real => bool list => bool"
166 "make_fun_by_explicit f_f v_v eqs =
167 (let h_h = (hd o (filterVar f_f)) eqs;
168 e_1 = hd (dropWhile (ident h_h) eqs);
169 v_s = dropWhile (ident f_f) (Vars h_h);
170 v_1 = hd (dropWhile (ident v_v) v_s);
171 s_1 = SubProblem(''DiffApp'', [''univariate'', ''equation''], [''no_met''])
173 in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "
174 setup \<open>KEStore_Elems.add_mets
175 [MethodC.prep_input thy "met_diffapp_funexp" [] MethodC.id_empty
176 (["DiffApp", "make_fun_by_explicit"],
177 [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
178 ("#Find" ,["functionEq f_1"])],
179 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=prog_expr,prls=Rule_Set.empty, crls = eval_rls,
180 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
181 @{thm make_fun_by_explicit.simps})]
183 setup \<open>KEStore_Elems.add_mets
184 [MethodC.prep_input thy "met_diffapp_max_oninterval" [] MethodC.id_empty
185 (["DiffApp", "max_on_interval_by_calculus"],
186 [("#Given" ,["functionEq t_t", "boundVariable v_v", "interval i_tv"(*, "errorBound e_rr"*)]),
187 ("#Find" ,["maxArgument v_0"])],
188 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
189 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
191 MethodC.prep_input thy "met_diffapp_findvals" [] MethodC.id_empty
192 (["DiffApp", "find_values"], [],
193 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
194 errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)},
198 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr
199 [Rule.Thm ("filterVar_Const", ThmC.numerals_to_Free @{thm filterVar_Const}),
200 Rule.Thm ("filterVar_Nil", ThmC.numerals_to_Free @{thm filterVar_Nil})];
202 setup_rule prog_expr = \<open>prog_expr\<close>