1 (* Title: "MathEngine/step.sml"
5 "-----------------------------------------------------------------------------------------------";
6 "table of contents -----------------------------------------------------------------------------";
7 "-----------------------------------------------------------------------------------------------";
8 "-----------------------------------------------------------------------------------------------";
9 "----------- survey on istate, context ----- ---------------------------------------------------";
10 "----------- embed fun Step.inconsistent -------------------------------------------------------";
11 "----------- maximum example with Step.specify_do_next -----------------------------------------";
12 (*"----------- maximum example with 'specify', fmz <> [] -----------------------------------------";*)
13 (*"----------- maximum example with 'specify', fmz = [] ------------------------------------------";*)
14 "-----------------------------------------------------------------------------------------------";
15 "-----------------------------------------------------------------------------------------------";
16 "-----------------------------------------------------------------------------------------------";
18 "----------- survey on istate, context ----- ---------------------------------------------------";
19 "----------- survey on istate, context ----- ---------------------------------------------------";
20 "----------- survey on istate, context ----- ---------------------------------------------------";
21 (* run this ---vvv code * )
22 "----------- fun me_trace all Minisubpbl -------------------------------------------------------";
23 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
25 ("Test", ["sqroot-test", "univariate", "equation", "test"],
26 ["Test", "squ-equ-test-subpbl1"]);
27 (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];(*Model_Problem*)
28 (*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
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 (*[], Met*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
35 (*[1], Frm*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
36 (*[1], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Rewrite_Set "norm_equation"*)
37 (*[2], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Rewrite_Set "Test_simplify"*)
38 (*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]*)
39 (*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
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], Met*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
46 (*[3, 1], Frm*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Apply_Method ["Test", "solve_linear"]*)
47 (*[3, 1], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv")*)
48 (*[3, 2], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Rewrite_Set "Test_simplify"*)
49 (*[3], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
50 (*[4], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Check_elementwise "Assumptions"*)
51 (*[], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
52 (*[], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*End_Proof'*)
53 ( * run this --- \<up> code *)
56 ========= ([], Pbl)========= Step.by_tactic: Model_Problem ==================================
57 Frm ..... (SOME (Pstate ([], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, false),
60 --------- ([], Pbl)--------- Step.do_next \<rightarrow> Add_Given equality (x + 1 = 2)----------------------------------
61 ========= ([], Met)========= Step.by_tactic: Apply_Method ["Test", "squ-equ-test-subpbl1"] ==================================
62 Frm ..... (SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),
63 ... ctxt: ["precond_rootmet x"]) ,
65 --------- ([1], Frm)--------- Step.do_next \<rightarrow> Rewrite_Set "norm_equation"----------------------------------
66 Frm ..... (SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),
67 ... ctxt: ["precond_rootmet x"]) ,
68 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),
69 ... ctxt: ["precond_rootmet x"]) )
70 ========= ([1], Frm)========= Step.by_tactic: Rewrite_Set "norm_equation" ==================================
71 Frm ..... (SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),
72 ... ctxt: ["precond_rootmet x"]) ,
73 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),
74 ... ctxt: ["precond_rootmet x"]) )
75 --------- ([1], Res)--------- Step.do_next \<rightarrow> Rewrite_Set "Test_simplify"----------------------------------
77 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),
78 ... ctxt: ["precond_rootmet x"]) )
79 ========= ([1], Res)========= Step.by_tactic: Rewrite_Set "Test_simplify" ==================================
81 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),
82 ... ctxt: ["precond_rootmet x"]) )
83 --------- ([2], Res)--------- Step.do_next \<rightarrow> Subproblem (Test, ["LINEAR", "univariate", "equation", "test"])----------------------------------
84 Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, Subproblem
86 ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''
87 ''test''), ORundef, true, false),
88 ... ctxt: ["precond_rootmet x"]) ,
90 ========= ([2], Res)========= Step.by_tactic: Subproblem (Test, ["LINEAR", "univariate", "equation", "test"]) ==================================
91 Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, Subproblem
93 ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''
94 ''test''), ORundef, true, true),
97 --------- ([3], Pbl)--------- Step.do_next \<rightarrow> Model_Problem ----------------------------------
98 ========= ([3], Pbl)========= Step.by_tactic: Model_Problem ==================================
99 Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, Subproblem
101 ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''
102 ''test''), ORundef, true, true),
105 --------- ([3], Pbl)--------- Step.do_next \<rightarrow> Add_Given equality (-1 + x = 0)----------------------------------
106 ========= ([3], Met)========= Step.by_tactic: Apply_Method ["Test", "solve_linear"] ==================================
107 Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),
108 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) ,
110 --------- ([3,1], Frm)--------- Step.do_next \<rightarrow> Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv")----------------------------------
111 Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),
112 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) ,
113 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),
114 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) )
115 ========= ([3,1], Frm)========= Step.by_tactic: Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv") ==================================
116 Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),
117 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) ,
118 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),
119 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) )
120 --------- ([3,1], Res)--------- Step.do_next \<rightarrow> Rewrite_Set "Test_simplify"----------------------------------
122 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),
123 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) )
124 ========= ([3,1], Res)========= Step.by_tactic: Rewrite_Set "Test_simplify" ==================================
126 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),
127 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) )
128 --------- ([3,2], Res)--------- Step.do_next \<rightarrow> Check_Postcond ["LINEAR", "univariate", "equation", "test"]----------------------------------
129 Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, Subproblem
131 ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''
132 ''test''), ORundef, true, true),
134 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),
135 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) )
136 ========= ([3,2], Res)========= Step.by_tactic: Check_Postcond ["LINEAR", "univariate", "equation", "test"] ==================================
137 Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, Subproblem
139 ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''
140 ''test''), ORundef, true, true),
142 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),
143 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) )
144 --------- ([3], Res)--------- Step.do_next \<rightarrow> Check_elementwise "Assumptions"----------------------------------
146 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),
147 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) )
148 ========= ([3], Res)========= Step.by_tactic: Check_elementwise "Assumptions" ==================================
150 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),
151 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) )
152 --------- ([4], Res)--------- Step.do_next \<rightarrow> Check_Postcond ["sqroot-test", "univariate", "equation", "test"]----------------------------------
153 Frm ..... (SOME (Pstate ([], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, false),
155 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),
156 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) )
157 ========= ([4], Res)========= Step.by_tactic: Check_Postcond ["sqroot-test", "univariate", "equation", "test"] ==================================
158 Frm ..... (SOME (Pstate ([], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, false),
160 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),
161 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) )
162 --------- ([], Res)--------- Step.do_next \<rightarrow> input End_Proof'----------------------------------
163 ========= ([], Res)========= Step.by_tactic: input End_Proof' ==================================
164 Frm ..... (SOME (Pstate ([], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, false),
166 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),
167 ... ctxt: ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) )
168 --------- ([], Res)--------- Step.do_next \<rightarrow> input End_Proof'----------------------------------
172 "--------- embed fun Step.inconsistent -------------------";
173 "--------- embed fun Step.inconsistent -------------------";
174 "--------- embed fun Step.inconsistent -------------------";
177 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
178 ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
181 autoCalculate 1 CompleteCalcHead;
182 autoCalculate 1 (Steps 1);
183 autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))*)
185 @{term "d_d x (x \<up> 2) + cos (4 * x \<up> 3)" }
187 appendFormula 1 "d_d x (x \<up> 2) + cos (4 * x \<up> 3)";
188 (*WAS ERROR: Inner syntax error \n Failed to parse term: "d_d x (x ^ 2) + cos (4 * x ^ 3)"
189 -----------------------------------------------------------------\<up>-----------------\<up>*)
190 (*/------------------- locate ERROR within appendFormula more precisely ---------------------\*)
191 "~~~~~ fun appendFormula , args:"; val (cI, ifo) = (1, "d_d x (x \<up> 2) + cos (4 * x \<up> 3)");
192 val cs = States.get_calc cI
193 val pos = States.get_pos cI 1
194 val ("ok", (_, _, ptp)) =
195 (*case*) Step.do_next pos cs (*of*);
197 (*case*) Step_Solve.by_term ptp (encode ifo) (*of*); (*WAS ERROR: Inner syntax error \n Failed to parse term*)
198 (*\------------------- locate ERROR within appendFormula more precisely ---------------------/*)
200 (* the check for errpat is maximally liberal (whole term modulo "rew_rls" from "type met"),
201 would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
202 results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
203 instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
204 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
205 findFillpatterns 1 "chain-rule-diff-both";
206 (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =
207 d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
209 "~~~~~ fun requestFillformula, args:"; val (cI, (errpatID, fillpatID)) =
210 (1, ("chain-rule-diff-both", "fill-both-args"));
211 val ((pt, _), _) = States.get_calc cI
212 val pos as (p, _) = States.get_pos cI 1;
213 val fillforms = Error_Pattern.find_fill_patterns (pt, pos) errpatID;
215 if pos = ([1], Res) then () else error "Step.inconsistent changed 1";
217 val (_, fillform, thm, sube_opt) :: _ = filter ((curry op = fillpatID) o
218 (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms;
220 "~~~~~ fun Step.inconsistent, args:";
221 val ((subs_opt, thm'), f', (is, ctxt), pos, pt) =
222 ((sube_opt, thm'_of_thm thm), fillform, (get_loc pt pos), pos, pt);
224 val f = get_curr_formula (pt, pos);
225 val pos' as (p', _) = (lev_on p, Res);
227 if pos = ([1], Res) then () else error "Step.inconsistent changed 2a";
228 if UnparseC.term @{context} f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
229 then () else error "Step.inconsistent changed 2b";
233 NONE => cappend_atomic pt p' (is, ContextC.insert_assumptions [] ctxt) f
234 (Rewrite thm') (f', []) Inconsistent
235 | SOME subs => cappend_atomic pt p' (is, ContextC.insert_assumptions [] ctxt) f
236 (Rewrite_Inst (subs, thm')) (f', []) Inconsistent
237 val pt = update_branch pt p' TransitiveB;
239 if get_obj g_tac pt p' = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", ""))
240 andalso pos = ([1], Res) andalso pos' = ([2], Res) andalso p' = [2]
241 then () else error "Step.inconsistent changed 3";
243 "~~~~~ to requestFillformula return val:"; val (pt, pos') = (pt, pos');
244 (*val (pt, pos') = Step.inconsistent (sube_opt, thm'_of_thm thm)
245 (fillform, []) (get_loc pt pos) pos' pt*)
246 States.upd_calc cI ((pt, pos'), []); States.upd_ipos cI 1 pos';
248 "~~~~~ final check:";
249 val ((pt, _),_) = States.get_calc 1;
250 val p = States.get_pos 1 1;
251 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
252 if p = ([2], Res) andalso
253 get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", "")) andalso
254 UnparseC.term @{context} f =
255 "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"
256 (*WAS with old findFillpatterns:
257 "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"
259 "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"
261 "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"*)
262 then () else error "Step.inconsistent changed: fill-formula?";
264 Test_Tool.show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*)
265 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
268 (*** maximum example with Step.specify_do_next ============================================= ***);
269 "----------- maximum example with Step.specify_do_next -----------------------------------------";
270 "----------- maximum example with Step.specify_do_next -----------------------------------------";
273 "fixedValues [r=Arbfix]", "maximum A",
274 "valuesFor [a,b::real]",
275 "relations [A=a*(b::real), (a/2) \<up> 2 + (b/2) \<up> 2 = (r::real) \<up> 2]",
276 "relations [A=a*(b::real), (a/2) \<up> 2 + (b/2) \<up> 2 = (r::real) \<up> 2]",
277 "relations [A=a*(b::real), a/2=r*sin alpha, b/2 = (r::real)*cos (alpha::real)]",
279 "boundVariable a", "boundVariable b", "boundVariable alpha",
280 "interval {x::real. 0 <= x & x <= 2*r}",
281 "interval {x::real. 0 <= x & x <= 2*r}",
282 "interval {x::real. 0 <= x & x <= pi}",
283 "errorBound (eps=(0::real))"];
284 val (dI',pI',mI') = ("Diff_App", ["maximum_of", "function"], ["Diff_App", "max_by_calculus"]);
285 val (p,_,f, nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
287 (*** stepwise Specification: Problem model================================================= ***)
288 val ("ok", ([(Model_Problem, Model_Problem' (["maximum_of", "function"], _, _), _)], _, ptp))
289 = Step.specify_do_next (pt, p);
290 val ("ok", ([(Add_Given "fixedValues [r = Arbfix]", _, _)], _, ptp))
291 = Step.specify_do_next ptp;
292 val ("ok", ([(Add_Find "maximum A", _, _)], _, ptp))
293 = Step.specify_do_next ptp;
294 val ("ok", ([(Add_Find "valuesFor [a]", _, _)], _, ptp))
295 = Step.specify_do_next ptp;
296 val ("ok", ([(Add_Find "valuesFor [a, b]", _, _)], _, ptp))
297 = Step.specify_do_next ptp;
298 val ("ok", ([(Add_Relation "relations [A = a * b]", _, _)], _, ptp))
299 = Step.specify_do_next ptp;
300 val ("ok", ([(Add_Relation "relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]", _, _)], _, ptp))
301 = Step.specify_do_next ptp;
303 (*** Problem model is complete ============================================================ ***)
304 val PblObj {probl, ...} = get_obj I (fst ptp) [];
306 val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS fixedValues [r = Arbfix] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS valuesFor [a, b] , pen2str, Position.T)), \n(4, [1, 2], true ,#Relate, (Cor_POS relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
307 = probl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt
309 (*** Specification of References ========================================================== ***)
310 val ("ok", ([(Specify_Theory "Diff_App", _, _)], _, ptp))
311 = Step.specify_do_next ptp;
312 val ("ok", ([(Specify_Problem ["maximum_of", "function"], _, _)], _, ptp))
313 = Step.specify_do_next ptp;
314 val ("ok", ([(Specify_Method ["Diff_App", "max_by_calculus"], _, _)], _, ptp))
315 = Step.specify_do_next ptp;
317 (*** stepwise Specification: MethodC model ================================================ ***)
318 val ("ok", ([(Add_Given "boundVariable a", _, _)], _, ptp))
319 = Step.specify_do_next ptp;
320 Step.specify_do_next ptp;
321 val ("ok", ([(Add_Given "interval {x. 0 \<le> x \<and> x \<le> 2 * r}", _, _)], _, ptp))
322 = Step.specify_do_next ptp;
323 val ("ok", ([(Add_Given "errorBound (eps = 0)", _, _)], _, ptp))
324 = Step.specify_do_next ptp;
326 val PblObj {meth, ...} = get_obj I (fst ptp) [];
328 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS fixedValues [r = Arbfix] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS maximum A , pen2str, Position.T)), \n(4, [1, 2], true ,#Relate, (Cor_POS relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS valuesFor [a, b] , pen2str, Position.T)), \n(6, [1], true ,#Given, (Cor_POS boundVariable a , pen2str, Position.T)), \n(9, [1, 2], true ,#Given, (Cor_POS interval {x. 0 \<le> x \<and> x \<le> 2 * r} , pen2str, Position.T)), \n(11, [1, 2, 3], true ,#Given, (Cor_POS errorBound (eps = 0) , pen2str, Position.T))]"
329 = meth |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt
331 (*** Specification of Problem and MethodC model is complete, Solution starts ============== ***)
333 (* Step.specify_do_next ptp;
335 ----------------------------------------------------------------------
336 actual arg(s) missing for '["(#Find, (maxArgument, v_0))"]' i.e. should be 'copy-named' by '*_._'
340 (*------------------------------------------------------ after specify --> Step.specify_find_next
341 "----------- maximum example with 'specify', fmz <> [] -----------------------------------------";
342 "----------- maximum example with 'specify', fmz <> [] -----------------------------------------";
343 "----------- maximum example with 'specify', fmz <> [] -----------------------------------------";
345 ["fixedValues [r=Arbfix]", "maximum A",
347 "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
348 "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
349 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
351 "boundVariable a", "boundVariable b", "boundVariable alpha",
352 "interval {x::real. 0 <= x & x <= 2*r}",
353 "interval {x::real. 0 <= x & x <= 2*r}",
354 "interval {x::real. 0 <= x & x <= pi}",
355 "errorBound (eps=(0::real))"];
357 ("Diff_App",["maximum_of", "function"],
358 ["Diff_App", "max_by_calculus"]);
360 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
362 val nxt = tac2tac_ pt p nxt;
363 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt e_pos' [] pt;
364 val nxt = tac2tac_ pt p nxt;
365 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
366 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
368 val nxt = tac2tac_ pt p nxt;
369 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
370 (*val nxt = Add_Find "maximum (A::bool)" : tac*)
372 val nxt = tac2tac_ pt p nxt;
373 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
374 (*val nxt = Add_Find "valuesFor [(a::real)]" : tac*)
376 val nxt = tac2tac_ pt p nxt;
377 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
378 (*val nxt = Add_Find "valuesFor [(b::real)]" : tac*)
380 val nxt = tac2tac_ pt p nxt;
381 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
382 (*val nxt = Add_Relation "relations [A = a * b]" *)
384 val nxt = tac2tac_ pt p nxt;
385 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
386 (*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)
388 (*---------------------------- FIXXXXME.me !!! partial Add-Relation !!!
389 Step_Specify.by_tactic_input <> specify ?!
391 if nxt<>(Add_Relation
392 "relations [(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]")
393 then error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)
395 val nxt = tac2tac_ pt p nxt;
396 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
397 ------------------------------ FIXXXXME.me !!! ---*)
399 (*val nxt = Specify_Theory "Diff_App" : tac*)
401 val itms = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt itms);
403 val nxt = tac2tac_ pt p nxt;
404 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
405 (*val nxt = Specify_Problem ["maximum_of", "function"]*)
407 val nxt = tac2tac_ pt p nxt;
408 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
409 (*val nxt = Specify_Method ("Diff_App", "max_by_calculus")*)
411 val nxt = tac2tac_ pt p nxt;
412 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
413 (*val nxt = Add_Given "boundVariable a" : tac*)
415 val nxt = tac2tac_ pt p nxt;
416 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
417 (*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)
419 val nxt = tac2tac_ pt p nxt;
420 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
421 (*val nxt = Add_Given "errorBound (eps = #0)" : tac*)
423 val nxt = tac2tac_ pt p nxt;
424 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
425 (*val nxt = Apply_Method ("Diff_App", "max_by_calculus") *)
426 case nxt of (Apply_Method ["Diff_App", "max_by_calculus"]) => ()
427 | _ => error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus";
430 "----------- maximum example with 'specify', fmz = [] ------------------------------------------";
431 "----------- maximum example with 'specify', fmz = [] ------------------------------------------";
432 "----------- maximum example with 'specify', fmz = [] ------------------------------------------";
434 val (dI',pI',mI') = empty_spec;
437 (*val (p,_,f,(_,nxt),_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; !!!*)
438 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt e_pos' []
440 val nxt = tac2tac_ pt p nxt;
441 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
442 (*val nxt = Specify_Theory ThyC.id_empty : tac*)
444 val nxt = Specify_Theory "Diff_App";
445 val nxt = tac2tac_ pt p nxt;
446 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
447 (*val nxt = Specify_Problem Problem.id_empty : tac*)
449 val nxt = Specify_Problem ["maximum_of", "function"];
450 val nxt = tac2tac_ pt p nxt;
451 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
452 (*val nxt = Add_Given "fixedValues" : tac*)
454 val nxt = Add_Given "fixedValues [r=Arbfix]";
455 val nxt = tac2tac_ pt p nxt;
456 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
457 (*val nxt = Add_Find "maximum" : tac*)
459 val nxt = Add_Find "maximum A";
460 val nxt = tac2tac_ pt p nxt;
463 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
464 (*val nxt = Add_Find "valuesFor" : tac*)
466 val nxt = Add_Find "valuesFor [a]";
467 val nxt = tac2tac_ pt p nxt;
468 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
469 (*val nxt = Add_Relation "relations" ---
470 --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
472 (*========== inhibit exn 010830 =======================================================*)
473 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
474 if nxt<>(Add_Relation "relations []")
475 then error "test specify, fmz <> []: nxt <> Add_Relation.."
476 else (); (*different with show_types !!!*)
478 (*========== inhibit exn 010830 =======================================================*)
480 val nxt = Add_Relation "relations [(A=a+b)]";
481 val nxt = tac2tac_ pt p nxt;
482 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
483 (*val nxt = Specify_Method (ThyC.id_empty, MethodC.id_empty) : tac*)
485 val nxt = Specify_Method ["Diff_App", "max_by_calculus"];
486 val nxt = tac2tac_ pt p nxt;
487 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
488 (*val nxt = Add_Given "boundVariable" : tac*)
490 val nxt = Add_Given "boundVariable alpha";
491 val nxt = tac2tac_ pt p nxt;
492 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
493 (*val nxt = Add_Given "interval" : tac*)
495 val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";
496 val nxt = tac2tac_ pt p nxt;
497 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
498 (*val nxt = Add_Given "errorBound" : tac*)
500 val nxt = Add_Given "errorBound (eps=999)";
501 val nxt = tac2tac_ pt p nxt;
502 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;
503 (*val nxt = Apply_Method ("Diff_App", "max_by_calculus") *)
505 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
506 if nxt<>(Apply_Method ("Diff_App", "max_by_calculus"))
507 then error "test specify, fmz <> []: nxt <> Add_Relation.."
510 (* 2.4.00 nach Transfer specify -> hard_gen
511 val nxt = Apply_Method ("Diff_App", "max_by_calculus");
512 val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt; *)
513 (*val nxt = Empty_Tac : tac*)
514 ------------------------------------------------------ after specify --> Step.specify_find_next *)