61 \<close> |
61 \<close> |
62 setup \<open>KEStore_Elems.add_rlss [("eval_rls", (Context.theory_name @{theory}, eval_rls))]\<close> |
62 setup \<open>KEStore_Elems.add_rlss [("eval_rls", (Context.theory_name @{theory}, eval_rls))]\<close> |
63 |
63 |
64 (** problem types **) |
64 (** problem types **) |
65 setup \<open>KEStore_Elems.add_pbts |
65 setup \<open>KEStore_Elems.add_pbts |
66 [(Specify.prep_pbt thy "pbl_fun_max" [] Celem.e_pblID |
66 [(Specify.prep_pbt thy "pbl_fun_max" [] Spec.e_pblID |
67 (["maximum_of","function"], |
67 (["maximum_of","function"], |
68 [("#Given" ,["fixedValues f_ix"]), |
68 [("#Given" ,["fixedValues f_ix"]), |
69 ("#Find" ,["maximum m_m","valuesFor v_s"]), |
69 ("#Find" ,["maximum m_m","valuesFor v_s"]), |
70 ("#Relate",["relations r_s"])], |
70 ("#Relate",["relations r_s"])], |
71 Rule_Set.empty, NONE, [])), |
71 Rule_Set.empty, NONE, [])), |
72 (Specify.prep_pbt thy "pbl_fun_make" [] Celem.e_pblID |
72 (Specify.prep_pbt thy "pbl_fun_make" [] Spec.e_pblID |
73 (["make","function"], |
73 (["make","function"], |
74 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
74 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
75 ("#Find" ,["functionEq f_1"])], |
75 ("#Find" ,["functionEq f_1"])], |
76 Rule_Set.empty, NONE, [])), |
76 Rule_Set.empty, NONE, [])), |
77 (Specify.prep_pbt thy "pbl_fun_max_expl" [] Celem.e_pblID |
77 (Specify.prep_pbt thy "pbl_fun_max_expl" [] Spec.e_pblID |
78 (["by_explicit","make","function"], |
78 (["by_explicit","make","function"], |
79 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
79 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
80 ("#Find" ,["functionEq f_1"])], |
80 ("#Find" ,["functionEq f_1"])], |
81 Rule_Set.empty, NONE, [["DiffApp","make_fun_by_explicit"]])), |
81 Rule_Set.empty, NONE, [["DiffApp","make_fun_by_explicit"]])), |
82 (Specify.prep_pbt thy "pbl_fun_max_newvar" [] Celem.e_pblID |
82 (Specify.prep_pbt thy "pbl_fun_max_newvar" [] Spec.e_pblID |
83 (["by_new_variable","make","function"], |
83 (["by_new_variable","make","function"], |
84 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
84 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
85 (*WN.12.5.03: precond for distinction still missing*) |
85 (*WN.12.5.03: precond for distinction still missing*) |
86 ("#Find" ,["functionEq f_1"])], |
86 ("#Find" ,["functionEq f_1"])], |
87 Rule_Set.empty, NONE, [["DiffApp","make_fun_by_new_variable"]])), |
87 Rule_Set.empty, NONE, [["DiffApp","make_fun_by_new_variable"]])), |
88 (Specify.prep_pbt thy "pbl_fun_max_interv" [] Celem.e_pblID |
88 (Specify.prep_pbt thy "pbl_fun_max_interv" [] Spec.e_pblID |
89 (["on_interval","maximum_of","function"], |
89 (["on_interval","maximum_of","function"], |
90 [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"]), |
90 [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"]), |
91 (*WN.12.5.03: precond for distinction still missing*) |
91 (*WN.12.5.03: precond for distinction still missing*) |
92 ("#Find" ,["maxArgument v_0"])], |
92 ("#Find" ,["maxArgument v_0"])], |
93 Rule_Set.empty, NONE, [])), |
93 Rule_Set.empty, NONE, [])), |
94 (Specify.prep_pbt thy "pbl_tool" [] Celem.e_pblID |
94 (Specify.prep_pbt thy "pbl_tool" [] Spec.e_pblID |
95 (["tool"], [], Rule_Set.empty, NONE, [])), |
95 (["tool"], [], Rule_Set.empty, NONE, [])), |
96 (Specify.prep_pbt thy "pbl_tool_findvals" [] Celem.e_pblID |
96 (Specify.prep_pbt thy "pbl_tool_findvals" [] Spec.e_pblID |
97 (["find_values","tool"], |
97 (["find_values","tool"], |
98 [("#Given" ,["maxArgument m_ax","functionEq f_f","boundVariable v_v"]), |
98 [("#Given" ,["maxArgument m_ax","functionEq f_f","boundVariable v_v"]), |
99 ("#Find" ,["valuesFor v_ls"]), |
99 ("#Find" ,["valuesFor v_ls"]), |
100 ("#Relate",["additionalRels r_s"])], |
100 ("#Relate",["additionalRels r_s"])], |
101 Rule_Set.empty, NONE, []))]\<close> |
101 Rule_Set.empty, NONE, []))]\<close> |
102 |
102 |
103 |
103 |
104 (** methods, scripts not yet implemented **) |
104 (** methods, scripts not yet implemented **) |
105 setup \<open>KEStore_Elems.add_mets |
105 setup \<open>KEStore_Elems.add_mets |
106 [Specify.prep_met thy "met_diffapp" [] Celem.e_metID |
106 [Specify.prep_met thy "met_diffapp" [] Spec.e_metID |
107 (["DiffApp"], [], |
107 (["DiffApp"], [], |
108 {rew_ord'="tless_true", rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.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=[]*)}, |
109 crls = Atools_erls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}, |
110 @{thm refl})] |
110 @{thm refl})] |
111 \<close> |
111 \<close> |
123 [''DiffApp'', ''max_on_interval_by_calculus'']) |
123 [''DiffApp'', ''max_on_interval_by_calculus'']) |
124 [BOOL t_t, REAL v_v, REAL_SET itv_v] |
124 [BOOL t_t, REAL v_v, REAL_SET itv_v] |
125 in SubProblem (''DiffApp'',[''find_values'', ''tool''], [''Isac_Knowledge'', ''find_values'']) |
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)])" |
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 |
127 setup \<open>KEStore_Elems.add_mets |
128 [Specify.prep_met thy "met_diffapp_max" [] Celem.e_metID |
128 [Specify.prep_met thy "met_diffapp_max" [] Spec.e_metID |
129 (["DiffApp","max_by_calculus"], |
129 (["DiffApp","max_by_calculus"], |
130 [("#Given" ,["fixedValues f_ix","maximum m_m","relations r_s", "boundVariable v_v", |
130 [("#Given" ,["fixedValues f_ix","maximum m_m","relations r_s", "boundVariable v_v", |
131 "interval i_tv","errorBound e_rr"]), |
131 "interval i_tv","errorBound e_rr"]), |
132 ("#Find" ,["valuesFor v_s"]), |
132 ("#Find" ,["valuesFor v_s"]), |
133 ("#Relate",[])], |
133 ("#Relate",[])], |
150 [BOOL e_1, REAL v_1]; |
150 [BOOL e_1, REAL v_1]; |
151 s_2 = SubProblem (''DiffApp'', [''univariate'', ''equation''], [''no_met'']) |
151 s_2 = SubProblem (''DiffApp'', [''univariate'', ''equation''], [''no_met'']) |
152 [BOOL e_2, REAL v_2] |
152 [BOOL e_2, REAL v_2] |
153 in Substitute [(v_1 = (rhs o hd) s_1), (v_2 = (rhs o hd) s_2)] h_h)" |
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 |
154 setup \<open>KEStore_Elems.add_mets |
155 [Specify.prep_met thy "met_diffapp_funnew" [] Celem.e_metID |
155 [Specify.prep_met thy "met_diffapp_funnew" [] Spec.e_metID |
156 (["DiffApp","make_fun_by_new_variable"], |
156 (["DiffApp","make_fun_by_new_variable"], |
157 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
157 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
158 ("#Find" ,["functionEq f_1"])], |
158 ("#Find" ,["functionEq f_1"])], |
159 {rew_ord'="tless_true",rls'=eval_rls,srls=prog_expr,prls=Rule_Set.empty, calc=[], crls = eval_rls, |
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=[]*)}, |
160 errpats = [], nrls = norm_Rational(*,asm_rls=[],asm_thm=[]*)}, |
170 v_1 = hd (dropWhile (ident v_v) v_s); |
170 v_1 = hd (dropWhile (ident v_v) v_s); |
171 s_1 = SubProblem(''DiffApp'', [''univariate'', ''equation''], [''no_met'']) |
171 s_1 = SubProblem(''DiffApp'', [''univariate'', ''equation''], [''no_met'']) |
172 [BOOL e_1, REAL v_1] |
172 [BOOL e_1, REAL v_1] |
173 in Substitute [(v_1 = (rhs o hd) s_1)] h_h) " |
173 in Substitute [(v_1 = (rhs o hd) s_1)] h_h) " |
174 setup \<open>KEStore_Elems.add_mets |
174 setup \<open>KEStore_Elems.add_mets |
175 [Specify.prep_met thy "met_diffapp_funexp" [] Celem.e_metID |
175 [Specify.prep_met thy "met_diffapp_funexp" [] Spec.e_metID |
176 (["DiffApp","make_fun_by_explicit"], |
176 (["DiffApp","make_fun_by_explicit"], |
177 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
177 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
178 ("#Find" ,["functionEq f_1"])], |
178 ("#Find" ,["functionEq f_1"])], |
179 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=prog_expr,prls=Rule_Set.empty, crls = eval_rls, |
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=[]*)}, |
180 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}, |
181 @{thm make_fun_by_explicit.simps})] |
181 @{thm make_fun_by_explicit.simps})] |
182 \<close> |
182 \<close> |
183 setup \<open>KEStore_Elems.add_mets |
183 setup \<open>KEStore_Elems.add_mets |
184 [Specify.prep_met thy "met_diffapp_max_oninterval" [] Celem.e_metID |
184 [Specify.prep_met thy "met_diffapp_max_oninterval" [] Spec.e_metID |
185 (["DiffApp","max_on_interval_by_calculus"], |
185 (["DiffApp","max_on_interval_by_calculus"], |
186 [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"(*, "errorBound e_rr"*)]), |
186 [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"(*, "errorBound e_rr"*)]), |
187 ("#Find" ,["maxArgument v_0"])], |
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, |
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=[]*)}, |
189 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}, |
190 @{thm refl}), |
190 @{thm refl}), |
191 Specify.prep_met thy "met_diffapp_findvals" [] Celem.e_metID |
191 Specify.prep_met thy "met_diffapp_findvals" [] Spec.e_metID |
192 (["DiffApp","find_values"], [], |
192 (["DiffApp","find_values"], [], |
193 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls, |
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 = []*)}, |
194 errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)}, |
195 @{thm refl})] |
195 @{thm refl})] |
196 \<close> |
196 \<close> |