1 (* Title: "MathEngine/step.sml"
3 (c) due to copyright terms
6 "-----------------------------------------------------------------------------------------------";
7 "table of contents -----------------------------------------------------------------------------";
8 "-----------------------------------------------------------------------------------------------";
9 "-----------------------------------------------------------------------------------------------";
10 "----------- survey on istate, context ----- ---------------------------------------------------";
11 "----------- embed fun Step.inconsistent -------------------------------------------------------";
12 "----------- maximum example with Step.specify_do_next -----------------------------------------";
13 (*"----------- maximum example with 'specify', fmz <> [] -----------------------------------------";*)
14 (*"----------- maximum example with 'specify', fmz = [] ------------------------------------------";*)
15 "-----------------------------------------------------------------------------------------------";
16 "-----------------------------------------------------------------------------------------------";
17 "-----------------------------------------------------------------------------------------------";
19 "----------- survey on istate, context ----- ---------------------------------------------------";
20 "----------- survey on istate, context ----- ---------------------------------------------------";
21 "----------- survey on istate, context ----- ---------------------------------------------------";
22 (* run this ---vvv code * )
23 "----------- fun me_trace all Minisubpbl -------------------------------------------------------";
24 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
26 ("Test", ["sqroot-test", "univariate", "equation", "test"],
27 ["Test", "squ-equ-test-subpbl1"]);
28 (*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];(*Model_Problem*)
29 (*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
30 (*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
31 (*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
32 (*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
33 (*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
34 (*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
35 (*[], Met*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
36 (*[1], Frm*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
37 (*[1], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Rewrite_Set "norm_equation"*)
38 (*[2], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Rewrite_Set "Test_simplify"*)
39 (*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]*)
40 (*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
41 (*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
42 (*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
43 (*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
44 (*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
45 (*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
46 (*[3], Met*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
47 (*[3, 1], Frm*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Apply_Method ["Test", "solve_linear"]*)
48 (*[3, 1], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv")*)
49 (*[3, 2], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Rewrite_Set "Test_simplify"*)
50 (*[3], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
51 (*[4], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Check_elementwise "Assumptions"*)
52 (*[], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
53 (*[], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*End_Proof'*)
54 ( * run this --- \<up> code *)
57 ========= ([], Pbl)========= Step.by_tactic: Model_Problem ==================================
58 Frm ..... (SOME (Pstate ([], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, false),
61 --------- ([], Pbl)--------- Step.do_next \<rightarrow> Add_Given equality (x + 1 = 2)----------------------------------
62 ========= ([], Met)========= Step.by_tactic: Apply_Method ["Test", "squ-equ-test-subpbl1"] ==================================
63 Frm ..... (SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),
64 ... ctxt: ["precond_rootmet x"]) ,
66 --------- ([1], Frm)--------- Step.do_next \<rightarrow> Rewrite_Set "norm_equation"----------------------------------
67 Frm ..... (SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),
68 ... ctxt: ["precond_rootmet x"]) ,
69 Res ..... SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [R,L,R,L,L,R,R], Rule_Set.empty, SOME e_e, x + 1 + -1 * 2 = 0, ORundef, true, false),
70 ... ctxt: ["precond_rootmet x"]) )
71 ========= ([1], Frm)========= Step.by_tactic: Rewrite_Set "norm_equation" ==================================
72 Frm ..... (SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),
73 ... ctxt: ["precond_rootmet x"]) ,
74 Res ..... SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [R,L,R,L,L,R,R], Rule_Set.empty, SOME e_e, x + 1 + -1 * 2 = 0, ORundef, true, true),
75 ... ctxt: ["precond_rootmet x"]) )
76 --------- ([1], Res)--------- Step.do_next \<rightarrow> Rewrite_Set "Test_simplify"----------------------------------
78 Res ..... SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [R,L,R,L,R,R], Rule_Set.empty, SOME e_e, -1 + x = 0, ORundef, true, false),
79 ... ctxt: ["precond_rootmet x"]) )
80 ========= ([1], Res)========= Step.by_tactic: Rewrite_Set "Test_simplify" ==================================
82 Res ..... SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [R,L,R,L,R,R], Rule_Set.empty, SOME e_e, -1 + x = 0, ORundef, true, false),
83 ... ctxt: ["precond_rootmet x"]) )
84 --------- ([2], Res)--------- Step.do_next \<rightarrow> Subproblem (Test, ["LINEAR", "univariate", "equation", "test"])----------------------------------
85 Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, Subproblem
87 ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''
88 ''test''), ORundef, true, false),
89 ... ctxt: ["precond_rootmet x"]) ,
91 ========= ([2], Res)========= Step.by_tactic: Subproblem (Test, ["LINEAR", "univariate", "equation", "test"]) ==================================
92 Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, Subproblem
94 ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''
95 ''test''), ORundef, true, true),
98 --------- ([3], Pbl)--------- Step.do_next \<rightarrow> Model_Problem ----------------------------------
99 ========= ([3], Pbl)========= Step.by_tactic: Model_Problem ==================================
100 Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, Subproblem
102 ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''
103 ''test''), ORundef, true, true),
106 --------- ([3], Pbl)--------- Step.do_next \<rightarrow> Add_Given equality (-1 + x = 0)----------------------------------
107 ========= ([3], Met)========= Step.by_tactic: Apply_Method ["Test", "solve_linear"] ==================================
108 Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),
109 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) ,
111 --------- ([3,1], Frm)--------- Step.do_next \<rightarrow> Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv")----------------------------------
112 Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),
113 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) ,
114 Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,L,R,L,R,L,R], Rule_Set.empty, SOME e_e, x = 0 + -1 * -1, ORundef, true, false),
115 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) )
116 ========= ([3,1], Frm)========= Step.by_tactic: Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv") ==================================
117 Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),
118 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) ,
119 Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,L,R,L,R,L,R], Rule_Set.empty, SOME e_e, x = 0 + -1 * -1, ORundef, true, true),
120 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) )
121 --------- ([3,1], Res)--------- Step.do_next \<rightarrow> Rewrite_Set "Test_simplify"----------------------------------
123 Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,L,R,L,R,R], Rule_Set.empty, SOME e_e, x = 1, ORundef, true, false),
124 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) )
125 ========= ([3,1], Res)========= Step.by_tactic: Rewrite_Set "Test_simplify" ==================================
127 Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,L,R,L,R,R], Rule_Set.empty, SOME e_e, x = 1, ORundef, true, false),
128 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) )
129 --------- ([3,2], Res)--------- Step.do_next \<rightarrow> Check_Postcond ["LINEAR", "univariate", "equation", "test"]----------------------------------
130 Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, Subproblem
132 ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''
133 ''test''), ORundef, true, true),
135 Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, [x = 1], ORundef, true, true),
136 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) )
137 ========= ([3,2], Res)========= Step.by_tactic: Check_Postcond ["LINEAR", "univariate", "equation", "test"] ==================================
138 Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, Subproblem
140 ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''
141 ''test''), ORundef, true, true),
143 Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, [x = 1], ORundef, true, true),
144 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) )
145 --------- ([3], Res)--------- Step.do_next \<rightarrow> Check_elementwise "Assumptions"----------------------------------
147 Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], Rule_Set.empty, NONE, [x = 1], ORundef, true, false),
148 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) )
149 ========= ([3], Res)========= Step.by_tactic: Check_elementwise "Assumptions" ==================================
151 Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], Rule_Set.empty, NONE, [x = 1], ORundef, true, true),
152 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) )
153 --------- ([4], Res)--------- Step.do_next \<rightarrow> Check_Postcond ["sqroot-test", "univariate", "equation", "test"]----------------------------------
154 Frm ..... (SOME (Pstate ([], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, false),
156 Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], Rule_Set.empty, NONE, [x = 1], ORundef, true, true),
157 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) )
158 ========= ([4], Res)========= Step.by_tactic: Check_Postcond ["sqroot-test", "univariate", "equation", "test"] ==================================
159 Frm ..... (SOME (Pstate ([], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, false),
161 Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], Rule_Set.empty, NONE, [x = 1], ORundef, true, true),
162 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) )
163 --------- ([], Res)--------- Step.do_next \<rightarrow> input End_Proof'----------------------------------
164 ========= ([], Res)========= Step.by_tactic: input End_Proof' ==================================
165 Frm ..... (SOME (Pstate ([], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, false),
167 Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], Rule_Set.empty, NONE, [x = 1], ORundef, true, true),
168 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) )
169 --------- ([], Res)--------- Step.do_next \<rightarrow> input End_Proof'----------------------------------
173 "--------- embed fun Step.inconsistent -------------------";
174 "--------- embed fun Step.inconsistent -------------------";
175 "--------- embed fun Step.inconsistent -------------------";
178 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
179 ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
182 autoCalculate 1 CompleteCalcHead;
183 autoCalculate 1 (Steps 1);
184 autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))*)
185 appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*);
186 (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
187 would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
188 results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
189 instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
190 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
191 findFillpatterns 1 "chain-rule-diff-both";
192 (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =
193 d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
195 "~~~~~ fun requestFillformula, args:"; val (cI, (errpatID, fillpatID)) =
196 (1, ("chain-rule-diff-both", "fill-both-args"));
197 val ((pt, _), _) = States.get_calc cI
198 val pos as (p, _) = States.get_pos cI 1;
199 val fillforms = Error_Pattern.find_fill_patterns (pt, pos) errpatID;
201 if pos = ([1], Res) then () else error "Step.inconsistent changed 1";
203 val (_, fillform, thm, sube_opt) :: _ = filter ((curry op = fillpatID) o
204 (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms;
206 "~~~~~ fun Step.inconsistent, args:";
207 val ((subs_opt, thm'), f', (is, ctxt), pos, pt) =
208 ((sube_opt, thm'_of_thm thm), fillform, (get_loc pt pos), pos, pt);
210 val f = get_curr_formula (pt, pos);
211 val pos' as (p', _) = (lev_on p, Res);
213 if pos = ([1], Res) then () else error "Step.inconsistent changed 2a";
214 if UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
215 then () else error "Step.inconsistent changed 2b";
219 NONE => cappend_atomic pt p' (is, ContextC.insert_assumptions [] ctxt) f
220 (Rewrite thm') (f', []) Inconsistent
221 | SOME subs => cappend_atomic pt p' (is, ContextC.insert_assumptions [] ctxt) f
222 (Rewrite_Inst (subs, thm')) (f', []) Inconsistent
223 val pt = update_branch pt p' TransitiveB;
225 if get_obj g_tac pt p' = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", ""))
226 andalso pos = ([1], Res) andalso pos' = ([2], Res) andalso p' = [2]
227 then () else error "Step.inconsistent changed 3";
229 "~~~~~ to requestFillformula return val:"; val (pt, pos') = (pt, pos');
230 (*val (pt, pos') = Step.inconsistent (sube_opt, thm'_of_thm thm)
231 (fillform, []) (get_loc pt pos) pos' pt*)
232 States.upd_calc cI ((pt, pos'), []); States.upd_ipos cI 1 pos';
234 "~~~~~ final check:";
235 val ((pt, _),_) = States.get_calc 1;
236 val p = States.get_pos 1 1;
237 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
238 if p = ([2], Res) andalso
239 get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", "")) andalso
241 "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos ?u * d_d x ?_dummy_2"
242 (*WAS with old findFillpatterns:
243 "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos ?_dummy_2 * d_d x ?_dummy_3"
245 "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos ?u * d_d x ?_dummy_2"
247 "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos ?_dummy_1 * d_d x ?_dummy_2"*)
248 then () else error "Step.inconsistent changed: fill-formula?";
250 Test_Tool.show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*)
251 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
254 (**** maximum example with Step.specify_do_next ########################################## ****)
255 "----------- maximum example with Step.specify_do_next -----------------------------------------";
256 "----------- maximum example with Step.specify_do_next -----------------------------------------";
259 "fixedValues [r=Arbfix]", "maximum A",
260 "valuesFor [a,b::real]",
261 "relations [A=a*(b::real), (a/2) \<up> 2 + (b/2) \<up> 2 = (r::real) \<up> 2]",
262 "relations [A=a*(b::real), (a/2) \<up> 2 + (b/2) \<up> 2 = (r::real) \<up> 2]",
263 "relations [A=a*(b::real), a/2=r*sin alpha, b/2 = (r::real)*cos (alpha::real)]",
265 "boundVariable a", "boundVariable b", "boundVariable alpha",
266 "interval {x::real. 0 <= x & x <= 2*r}",
267 "interval {x::real. 0 <= x & x <= 2*r}",
268 "interval {x::real. 0 <= x & x <= pi}",
269 "errorBound (eps=(0::real))"];
270 val (dI',pI',mI') = ("Diff_App", ["maximum_of", "function"], ["Diff_App", "max_by_calculus"]);
271 val (p,_,f, nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
273 (*** stepwise Specification: Problem model================================================= ***)
274 val ("ok", ([(Model_Problem, Model_Problem' (["maximum_of", "function"], _, _), _)], _, ptp))
275 = Step.specify_do_next (pt, p);
276 val ("ok", ([(Add_Given "fixedValues [r = Arbfix]", _, _)], _, ptp))
277 = Step.specify_do_next ptp;
278 val ("ok", ([(Add_Find "maximum A", _, _)], _, ptp))
279 = Step.specify_do_next ptp;
280 val ("ok", ([(Add_Find "valuesFor [a]", _, _)], _, ptp))
281 = Step.specify_do_next ptp;
282 val ("ok", ([(Add_Find "valuesFor [b]", _, _)], _, ptp))
283 = Step.specify_do_next ptp;
284 val ("ok", ([(Add_Relation "relations [A = a * b]", _, _)], _, ptp))
285 = Step.specify_do_next ptp;
286 val ("ok", ([(Add_Relation "relations [(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]", _, _)], _, ptp))
287 = Step.specify_do_next ptp;
289 (*** Problem model is complete ============================================================ ***)
290 val PblObj {probl, ...} = get_obj I (fst ptp) [];
292 if I_Model.to_string @{context} probl = "[\n" ^
293 "(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])), \n" ^
294 "(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A ,(m_m, [A])), \n" ^
295 "(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] ,(v_s, [[a, b]])), \n" ^
296 "(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(r_s, [[A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]"
297 then () else error "I_Model.to_string probl CHANGED";
299 (*** Specification of References ========================================================== ***)
300 val ("ok", ([(Specify_Theory "Diff_App", _, _)], _, ptp))
301 = Step.specify_do_next ptp;
302 val ("ok", ([(Specify_Problem ["maximum_of", "function"], _, _)], _, ptp))
303 = Step.specify_do_next ptp;
304 val ("ok", ([(Specify_Method ["Diff_App", "max_by_calculus"], _, _)], _, ptp))
305 = Step.specify_do_next ptp;
307 (*** stepwise Specification: MethodC model ================================================ ***)
308 val ("ok", ([(Add_Given "boundVariable a", _, _)], _, ptp))
309 = Step.specify_do_next ptp;
310 val ("ok", ([(Add_Given "interval {x. 0 \<le> x \<and> x \<le> 2 * r}", _, _)], _, ptp))
311 = Step.specify_do_next ptp;
312 val ("ok", ([(Add_Given "errorBound (eps = 0)", _, _)], _, ptp))
313 = Step.specify_do_next ptp;
315 val PblObj {meth, ...} = get_obj I (fst ptp) [];
316 if I_Model.to_string @{context} meth = "[\n" ^
317 "(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])), \n" ^
318 "(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A ,(m_m, [A])), \n" ^
319 "(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] ,(v_s, [[a, b]])), \n" ^
320 "(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(r_s, [[A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])), \n" ^
321 "(6 ,[1] ,true ,#Given ,Cor boundVariable a ,(v_v, [a])), \n" ^
322 "(9 ,[1, 2] ,true ,#Given ,Cor interval {x. 0 \<le> x \<and> x \<le> 2 * r} ,(i_tv, [{x. 0 \<le> x \<and> x \<le> 2 * r}])), \n" ^
323 "(11 ,[1, 2, 3] ,true ,#Given ,Cor errorBound (eps = 0) ,(e_rr, [eps = 0]))]"
324 then () else error "I_Model.to_string meth CHANGED";
325 (*** Specification of Problem and MethodC model is complete, Solution starts ============== ***)
327 (* Step.specify_do_next ptp;
329 ----------------------------------------------------------------------
330 actual arg(s) missing for '["(#Find, (maxArgument, v_0))"]' i.e. should be 'copy-named' by '*_._'
334 (*------------------------------------------------------ after specify --> Step.specify_find_next
335 "----------- maximum example with 'specify', fmz <> [] -----------------------------------------";
336 "----------- maximum example with 'specify', fmz <> [] -----------------------------------------";
337 "----------- maximum example with 'specify', fmz <> [] -----------------------------------------";
339 ["fixedValues [r=Arbfix]", "maximum A",
341 "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
342 "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
343 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
345 "boundVariable a", "boundVariable b", "boundVariable alpha",
346 "interval {x::real. 0 <= x & x <= 2*r}",
347 "interval {x::real. 0 <= x & x <= 2*r}",
348 "interval {x::real. 0 <= x & x <= pi}",
349 "errorBound (eps=(0::real))"];
351 ("Diff_App",["maximum_of", "function"],
352 ["Diff_App", "max_by_calculus"]);
354 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
356 val nxt = tac2tac_ pt p nxt;
357 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt e_pos' [] pt;
358 val nxt = tac2tac_ pt p nxt;
359 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
360 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
362 val nxt = tac2tac_ pt p nxt;
363 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
364 (*val nxt = Add_Find "maximum (A::bool)" : tac*)
366 val nxt = tac2tac_ pt p nxt;
367 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
368 (*val nxt = Add_Find "valuesFor [(a::real)]" : tac*)
370 val nxt = tac2tac_ pt p nxt;
371 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
372 (*val nxt = Add_Find "valuesFor [(b::real)]" : tac*)
374 val nxt = tac2tac_ pt p nxt;
375 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
376 (*val nxt = Add_Relation "relations [A = a * b]" *)
378 val nxt = tac2tac_ pt p nxt;
379 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
380 (*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)
382 (*---------------------------- FIXXXXME.me !!! partial Add-Relation !!!
383 Step_Specify.by_tactic_input <> specify ?!
385 if nxt<>(Add_Relation
386 "relations [(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]")
387 then error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)
389 val nxt = tac2tac_ pt p nxt;
390 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
391 ------------------------------ FIXXXXME.me !!! ---*)
393 (*val nxt = Specify_Theory "Diff_App" : tac*)
395 val itms = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt itms);
397 val nxt = tac2tac_ pt p nxt;
398 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
399 (*val nxt = Specify_Problem ["maximum_of", "function"]*)
401 val nxt = tac2tac_ pt p nxt;
402 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
403 (*val nxt = Specify_Method ("Diff_App", "max_by_calculus")*)
405 val nxt = tac2tac_ pt p nxt;
406 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
407 (*val nxt = Add_Given "boundVariable a" : tac*)
409 val nxt = tac2tac_ pt p nxt;
410 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
411 (*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)
413 val nxt = tac2tac_ pt p nxt;
414 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
415 (*val nxt = Add_Given "errorBound (eps = #0)" : tac*)
417 val nxt = tac2tac_ pt p nxt;
418 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
419 (*val nxt = Apply_Method ("Diff_App", "max_by_calculus") *)
420 case nxt of (Apply_Method ["Diff_App", "max_by_calculus"]) => ()
421 | _ => error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus";
424 "----------- maximum example with 'specify', fmz = [] ------------------------------------------";
425 "----------- maximum example with 'specify', fmz = [] ------------------------------------------";
426 "----------- maximum example with 'specify', fmz = [] ------------------------------------------";
428 val (dI',pI',mI') = empty_spec;
431 (*val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; !!!*)
432 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt e_pos' []
434 val nxt = tac2tac_ pt p nxt;
435 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
436 (*val nxt = Specify_Theory ThyC.id_empty : tac*)
438 val nxt = Specify_Theory "Diff_App";
439 val nxt = tac2tac_ pt p nxt;
440 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
441 (*val nxt = Specify_Problem Problem.id_empty : tac*)
443 val nxt = Specify_Problem ["maximum_of", "function"];
444 val nxt = tac2tac_ pt p nxt;
445 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
446 (*val nxt = Add_Given "fixedValues" : tac*)
448 val nxt = Add_Given "fixedValues [r=Arbfix]";
449 val nxt = tac2tac_ pt p nxt;
450 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
451 (*val nxt = Add_Find "maximum" : tac*)
453 val nxt = Add_Find "maximum A";
454 val nxt = tac2tac_ pt p nxt;
457 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
458 (*val nxt = Add_Find "valuesFor" : tac*)
460 val nxt = Add_Find "valuesFor [a]";
461 val nxt = tac2tac_ pt p nxt;
462 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
463 (*val nxt = Add_Relation "relations" ---
464 --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
466 (*========== inhibit exn 010830 =======================================================*)
467 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
468 if nxt<>(Add_Relation "relations []")
469 then error "test specify, fmz <> []: nxt <> Add_Relation.."
470 else (); (*different with show_types !!!*)
472 (*========== inhibit exn 010830 =======================================================*)
474 val nxt = Add_Relation "relations [(A=a+b)]";
475 val nxt = tac2tac_ pt p nxt;
476 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
477 (*val nxt = Specify_Method (ThyC.id_empty, MethodC.id_empty) : tac*)
479 val nxt = Specify_Method ["Diff_App", "max_by_calculus"];
480 val nxt = tac2tac_ pt p nxt;
481 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
482 (*val nxt = Add_Given "boundVariable" : tac*)
484 val nxt = Add_Given "boundVariable alpha";
485 val nxt = tac2tac_ pt p nxt;
486 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
487 (*val nxt = Add_Given "interval" : tac*)
489 val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";
490 val nxt = tac2tac_ pt p nxt;
491 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
492 (*val nxt = Add_Given "errorBound" : tac*)
494 val nxt = Add_Given "errorBound (eps=999)";
495 val nxt = tac2tac_ pt p nxt;
496 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
497 (*val nxt = Apply_Method ("Diff_App", "max_by_calculus") *)
499 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
500 if nxt<>(Apply_Method ("Diff_App", "max_by_calculus"))
501 then error "test specify, fmz <> []: nxt <> Add_Relation.."
504 (* 2.4.00 nach Transfer specify -> hard_gen
505 val nxt = Apply_Method ("Diff_App", "max_by_calculus");
506 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; *)
507 (*val nxt = Empty_Tac : tac*)
508 ------------------------------------------------------ after specify --> Step.specify_find_next *)