1 (* application of differential calculus
3 (c) due to copyright terms
6 theory DiffApp imports Diff begin
11 :: "[bool list,real,bool list,real,real set,bool,
12 bool list] => bool list"
13 ("((Script Maximum'_value (_ _ _ _ _ _ =))// (_))" 9)
15 Make'_fun'_by'_new'_variable
16 :: "[real,real,bool list,
18 ("((Script Make'_fun'_by'_new'_variable (_ _ _ =))// (_))" 9)
19 Make'_fun'_by'_explicit
20 :: "[real,real,bool list,
22 ("((Script Make'_fun'_by'_explicit (_ _ _ =))// (_))" 9)
26 (*for script Maximum_value*)
27 filterVar :: "[real, 'a list] => 'a list"
30 filterVar_Nil: "filterVar v [] = []" and
31 filterVar_Const: "filterVar v (x#xs) =
32 (if (v : set (Vars x)) then x#(filterVar v xs)
33 else filterVar v xs) "
34 text {*WN.6.5.03: old decisions in this file partially are being changed
35 in a quick-and-dirty way to make scripts run: Maximum_value,
36 Make_fun_by_new_variable, Make_fun_by_explicit.
37 found to be reconsidered:
38 - descriptions (Descript.thy)
39 - penv: really need term list; or just rerun the whole example with num/var
40 - mk_arg, itms2args ... env in script different from penv ?
41 - L = SubProblem eq ... show some vars on the worksheet ? (other means for
42 referencing are labels (no on worksheet))
44 WN.6.5.03 quick-and-dirty: mk_arg, itms2args just make most convenient env
51 val eval_rls = prep_rls' (
52 Celem.Rls {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI),
53 erls = Celem.e_rls, srls = Celem.Erls, calc = [], errpatts = [],
54 rules = [Celem.Thm ("refl", TermC.num_str @{thm refl}),
55 Celem.Thm ("order_refl", TermC.num_str @{thm order_refl}),
56 Celem.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
57 Celem.Thm ("not_true", TermC.num_str @{thm not_true}),
58 Celem.Thm ("not_false", TermC.num_str @{thm not_false}),
59 Celem.Thm ("and_true", TermC.num_str @{thm and_true}),
60 Celem.Thm ("and_false", TermC.num_str @{thm and_false}),
61 Celem.Thm ("or_true", TermC.num_str @{thm or_true}),
62 Celem.Thm ("or_false", TermC.num_str @{thm or_false}),
63 Celem.Thm ("and_commute", TermC.num_str @{thm and_commute}),
64 Celem.Thm ("or_commute", TermC.num_str @{thm or_commute}),
66 Celem.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
67 Celem.Calc ("Orderings.ord_class.less_eq", eval_equ "#less_equal_"),
69 Celem.Calc ("Atools.ident", eval_ident "#ident_"),
70 Celem.Calc ("Atools.is'_const", eval_const "#is_const_"),
71 Celem.Calc ("Atools.occurs'_in", eval_occurs_in ""),
72 Celem.Calc ("Tools.matches", eval_matches "")],
73 scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
76 setup {* KEStore_Elems.add_rlss [("eval_rls", (Context.theory_name @{theory}, eval_rls))] *}
79 setup {* KEStore_Elems.add_pbts
80 [(Specify.prep_pbt thy "pbl_fun_max" [] Celem.e_pblID
81 (["maximum_of","function"],
82 [("#Given" ,["fixedValues f_ix"]),
83 ("#Find" ,["maximum m_m","valuesFor v_s"]),
84 ("#Relate",["relations r_s"])],
85 Celem.e_rls, NONE, [])),
86 (Specify.prep_pbt thy "pbl_fun_make" [] Celem.e_pblID
88 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
89 ("#Find" ,["functionEq f_1"])],
90 Celem.e_rls, NONE, [])),
91 (Specify.prep_pbt thy "pbl_fun_max_expl" [] Celem.e_pblID
92 (["by_explicit","make","function"],
93 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
94 ("#Find" ,["functionEq f_1"])],
95 Celem.e_rls, NONE, [["DiffApp","make_fun_by_explicit"]])),
96 (Specify.prep_pbt thy "pbl_fun_max_newvar" [] Celem.e_pblID
97 (["by_new_variable","make","function"],
98 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
99 (*WN.12.5.03: precond for distinction still missing*)
100 ("#Find" ,["functionEq f_1"])],
101 Celem.e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]])),
102 (Specify.prep_pbt thy "pbl_fun_max_interv" [] Celem.e_pblID
103 (["on_interval","maximum_of","function"],
104 [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"]),
105 (*WN.12.5.03: precond for distinction still missing*)
106 ("#Find" ,["maxArgument v_0"])],
107 Celem.e_rls, NONE, [])),
108 (Specify.prep_pbt thy "pbl_tool" [] Celem.e_pblID
109 (["tool"], [], Celem.e_rls, NONE, [])),
110 (Specify.prep_pbt thy "pbl_tool_findvals" [] Celem.e_pblID
111 (["find_values","tool"],
112 [("#Given" ,["maxArgument m_ax","functionEq f_f","boundVariable v_v"]),
113 ("#Find" ,["valuesFor v_ls"]),
114 ("#Relate",["additionalRels r_s"])],
115 Celem.e_rls, NONE, []))] *}
118 (** methods, scripts not yet implemented **)
119 setup {* KEStore_Elems.add_mets
120 [Specify.prep_met thy "met_diffapp" [] Celem.e_metID
122 {rew_ord'="tless_true", rls'=Atools_erls,calc = [], srls = Celem.e_rls, prls = Celem.e_rls,
123 crls = Atools_erls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
125 Specify.prep_met thy "met_diffapp_max" [] Celem.e_metID
126 (["DiffApp","max_by_calculus"],
127 [("#Given" ,["fixedValues f_ix","maximum m_m","relations r_s", "boundVariable v_v",
128 "interval i_tv","errorBound e_rr"]),
129 ("#Find" ,["valuesFor v_s"]),
131 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=Celem.e_rls, crls = eval_rls,
132 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
133 "Script Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list) " ^
134 " (v_v::real) (itv_v::real set) (e_rr::bool) = " ^
135 " (let e_e = (hd o (filterVar m_m)) r_s; " ^
136 " t_t = (if 1 < LENGTH r_s " ^
137 " then (SubProblem (DiffApp',[make,function],[no_met]) " ^
138 " [REAL m_m, REAL v_v, BOOL_LIST r_s]) " ^
139 " else (hd r_s)); " ^
141 "SubProblem(DiffApp',[on_interval,maximum_of,function], " ^
142 " [DiffApp,max_on_interval_by_calculus]) " ^
143 " [BOOL t_t, REAL v_v, REAL_SET i_tv] " ^
144 " in ((SubProblem (DiffApp',[find_values,tool],[Isac,find_values]) " ^
145 " [REAL m_x, REAL (Rhs t_t), REAL v_v, REAL m_m, " ^
146 " BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list)) "),
147 Specify.prep_met thy "met_diffapp_funnew" [] Celem.e_metID
148 (["DiffApp","make_fun_by_new_variable"],
149 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
150 ("#Find" ,["functionEq f_1"])],
151 {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=Celem.e_rls, calc=[], crls = eval_rls,
152 errpats = [], nrls = norm_Rational(*,asm_rls=[],asm_thm=[]*)},
153 "Script Make_fun_by_new_variable (f_f::real) (v_v::real) " ^
154 " (eqs::bool list) = " ^
155 "(let h_h = (hd o (filterVar f_f)) eqs; " ^
156 " e_s = dropWhile (ident h_h) eqs; " ^
157 " v_s = dropWhile (ident f_f) (Vars h_h); " ^
158 " v_1 = NTH 1 v_s; " ^
159 " v_2 = NTH 2 v_s; " ^
160 " e_1 = (hd o (filterVar v_1)) e_s; " ^
161 " e_2 = (hd o (filterVar v_2)) e_s; " ^
162 " (s_1::bool list) = " ^
163 " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^
164 " [BOOL e_1, REAL v_1]); " ^
165 " (s_2::bool list) = " ^
166 " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^
167 " [BOOL e_2, REAL v_2])" ^
168 "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)"),
169 Specify.prep_met thy "met_diffapp_funexp" [] Celem.e_metID
170 (["DiffApp","make_fun_by_explicit"],
171 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
172 ("#Find" ,["functionEq f_1"])],
173 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=Celem.e_rls, crls = eval_rls,
174 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
175 "Script Make_fun_by_explicit (f_f::real) (v_v::real) " ^
176 " (eqs::bool list) = " ^
177 " (let h_h = (hd o (filterVar f_f)) eqs; " ^
178 " e_1 = hd (dropWhile (ident h_h) eqs); " ^
179 " v_s = dropWhile (ident f_f) (Vars h_h); " ^
180 " v_1 = hd (dropWhile (ident v_v) v_s); " ^
181 " (s_1::bool list)= " ^
182 " (SubProblem(DiffApp',[univariate,equation],[no_met])" ^
183 " [BOOL e_1, REAL v_1]) " ^
184 " in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "),
185 Specify.prep_met thy "met_diffapp_max_oninterval" [] Celem.e_metID
186 (["DiffApp","max_on_interval_by_calculus"],
187 [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"(*, "errorBound e_rr"*)]),
188 ("#Find" ,["maxArgument v_0"])],
189 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Celem.e_rls,prls=Celem.e_rls, crls = eval_rls,
190 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
192 Specify.prep_met thy "met_diffapp_findvals" [] Celem.e_metID
193 (["DiffApp","find_values"], [],
194 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Celem.e_rls,prls=Celem.e_rls, crls = eval_rls,
195 errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)},
199 val list_rls = Celem.append_rls "list_rls" list_rls
200 [Celem.Thm ("filterVar_Const", TermC.num_str @{thm filterVar_Const}),
201 Celem.Thm ("filterVar_Nil", TermC.num_str @{thm filterVar_Nil})];
203 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}