|
walther@59763
|
1 |
(* Title: "MathEngine/step.sml"
|
|
walther@59763
|
2 |
Author: Walther Neuper
|
|
walther@59763
|
3 |
(c) due to copyright terms
|
|
walther@59763
|
4 |
*)
|
|
walther@59763
|
5 |
|
|
walther@59763
|
6 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59763
|
7 |
"table of contents -----------------------------------------------------------------------------";
|
|
walther@59763
|
8 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59763
|
9 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59814
|
10 |
"----------- survey on istate, context ----- ---------------------------------------------------";
|
|
walther@59763
|
11 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59763
|
12 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59763
|
13 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59763
|
14 |
|
|
walther@59814
|
15 |
"----------- survey on istate, context ----- ---------------------------------------------------";
|
|
walther@59814
|
16 |
"----------- survey on istate, context ----- ---------------------------------------------------";
|
|
walther@59814
|
17 |
"----------- survey on istate, context ----- ---------------------------------------------------";
|
|
walther@59814
|
18 |
(* run this ---vvv code * )
|
|
walther@59814
|
19 |
"----------- fun me_trace all Minisubpbl -------------------------------------------------------";
|
|
walther@59814
|
20 |
val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
|
|
walther@59814
|
21 |
val (dI',pI',mI') =
|
|
walther@59814
|
22 |
("Test", ["sqroot-test","univariate","equation","test"],
|
|
walther@59814
|
23 |
["Test","squ-equ-test-subpbl1"]);
|
|
walther@59814
|
24 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];(*Model_Problem*)
|
|
walther@59814
|
25 |
(*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
|
|
walther@59814
|
26 |
(*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
|
|
walther@59814
|
27 |
(*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
|
|
walther@59814
|
28 |
(*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
|
|
walther@59814
|
29 |
(*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
|
|
walther@59814
|
30 |
(*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
|
|
walther@59814
|
31 |
(*[], Met*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
|
|
walther@59814
|
32 |
(*[1], Frm*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Apply_Method ["Test","squ-equ-test-subpbl1"]*)
|
|
walther@59814
|
33 |
(*[1], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Rewrite_Set "norm_equation"*)
|
|
walther@59814
|
34 |
(*[2], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Rewrite_Set "Test_simplify"*)
|
|
walther@59814
|
35 |
(*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]*)
|
|
walther@59814
|
36 |
(*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
|
|
walther@59814
|
37 |
(*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
|
|
walther@59814
|
38 |
(*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
|
|
walther@59814
|
39 |
(*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
|
|
walther@59814
|
40 |
(*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
|
|
walther@59814
|
41 |
(*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
|
|
walther@59814
|
42 |
(*[3], Met*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;
|
|
walther@59814
|
43 |
(*[3, 1], Frm*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Apply_Method ["Test","solve_linear"]*)
|
|
walther@59814
|
44 |
(*[3, 1], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv")*)
|
|
walther@59814
|
45 |
(*[3, 2], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Rewrite_Set "Test_simplify"*)
|
|
walther@59814
|
46 |
(*[3], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Check_Postcond ["LINEAR","univariate","equation","test"]*)
|
|
walther@59814
|
47 |
(*[4], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Check_elementwise "Assumptions"*)
|
|
walther@59814
|
48 |
(*[], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Check_Postcond ["sqroot-test","univariate","equation","test"]*)
|
|
walther@59814
|
49 |
(*[], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*End_Proof'*)
|
|
walther@59814
|
50 |
( * run this ---^^^code *)
|
|
walther@59814
|
51 |
|
|
walther@59814
|
52 |
(* for this output:
|
|
walther@59814
|
53 |
========= ([], Pbl)========= Step.by_tactic: Model_Problem ==================================
|
|
walther@59814
|
54 |
Frm ..... (SOME (Pstate ([], [], e_rls, NONE, ??.empty, ORundef, false, false),
|
|
walther@59814
|
55 |
... ctxt: []) ,
|
|
walther@59814
|
56 |
Res ..... NONE)
|
|
walther@59814
|
57 |
--------- ([], Pbl)--------- Step.do_next \<rightarrow> Add_Given equality (x + 1 = 2)----------------------------------
|
|
walther@59814
|
58 |
========= ([], Met)========= Step.by_tactic: Apply_Method ["Test","squ-equ-test-subpbl1"] ==================================
|
|
walther@59814
|
59 |
Frm ..... (SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [], e_rls, NONE, ??.empty, ORundef, false, true),
|
|
walther@59814
|
60 |
... ctxt: ["precond_rootmet x"]) ,
|
|
walther@59814
|
61 |
Res ..... NONE)
|
|
walther@59814
|
62 |
--------- ([1], Frm)--------- Step.do_next \<rightarrow> Rewrite_Set "norm_equation"----------------------------------
|
|
walther@59814
|
63 |
Frm ..... (SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [], e_rls, NONE, ??.empty, ORundef, false, true),
|
|
walther@59814
|
64 |
... ctxt: ["precond_rootmet x"]) ,
|
|
walther@59814
|
65 |
Res ..... SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [R,L,R,L,L,R,R], e_rls, SOME e_e, x + 1 + -1 * 2 = 0, ORundef, true, false),
|
|
walther@59814
|
66 |
... ctxt: ["precond_rootmet x"]) )
|
|
walther@59814
|
67 |
========= ([1], Frm)========= Step.by_tactic: Rewrite_Set "norm_equation" ==================================
|
|
walther@59814
|
68 |
Frm ..... (SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [], e_rls, NONE, ??.empty, ORundef, false, true),
|
|
walther@59814
|
69 |
... ctxt: ["precond_rootmet x"]) ,
|
|
walther@59814
|
70 |
Res ..... SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [R,L,R,L,L,R,R], e_rls, SOME e_e, x + 1 + -1 * 2 = 0, ORundef, true, true),
|
|
walther@59814
|
71 |
... ctxt: ["precond_rootmet x"]) )
|
|
walther@59814
|
72 |
--------- ([1], Res)--------- Step.do_next \<rightarrow> Rewrite_Set "Test_simplify"----------------------------------
|
|
walther@59814
|
73 |
Frm ..... (NONE,
|
|
walther@59814
|
74 |
Res ..... SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [R,L,R,L,R,R], e_rls, SOME e_e, -1 + x = 0, ORundef, true, false),
|
|
walther@59814
|
75 |
... ctxt: ["precond_rootmet x"]) )
|
|
walther@59814
|
76 |
========= ([1], Res)========= Step.by_tactic: Rewrite_Set "Test_simplify" ==================================
|
|
walther@59814
|
77 |
Frm ..... (NONE,
|
|
walther@59814
|
78 |
Res ..... SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [R,L,R,L,R,R], e_rls, SOME e_e, -1 + x = 0, ORundef, true, false),
|
|
walther@59814
|
79 |
... ctxt: ["precond_rootmet x"]) )
|
|
walther@59814
|
80 |
--------- ([2], Res)--------- Step.do_next \<rightarrow> Subproblem (Test, ["LINEAR","univariate","equation","test"])----------------------------------
|
|
walther@59814
|
81 |
Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], e_rls, NONE, Subproblem
|
|
walther@59814
|
82 |
(''Test'',
|
|
walther@59814
|
83 |
??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''
|
|
walther@59814
|
84 |
''test''), ORundef, true, false),
|
|
walther@59814
|
85 |
... ctxt: ["precond_rootmet x"]) ,
|
|
walther@59814
|
86 |
Res ..... NONE)
|
|
walther@59814
|
87 |
========= ([2], Res)========= Step.by_tactic: Subproblem (Test, ["LINEAR","univariate","equation","test"]) ==================================
|
|
walther@59814
|
88 |
Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], e_rls, NONE, Subproblem
|
|
walther@59814
|
89 |
(''Test'',
|
|
walther@59814
|
90 |
??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''
|
|
walther@59814
|
91 |
''test''), ORundef, true, true),
|
|
walther@59814
|
92 |
... ctxt: []) ,
|
|
walther@59814
|
93 |
Res ..... NONE)
|
|
walther@59814
|
94 |
--------- ([3], Pbl)--------- Step.do_next \<rightarrow> Model_Problem ----------------------------------
|
|
walther@59814
|
95 |
========= ([3], Pbl)========= Step.by_tactic: Model_Problem ==================================
|
|
walther@59814
|
96 |
Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], e_rls, NONE, Subproblem
|
|
walther@59814
|
97 |
(''Test'',
|
|
walther@59814
|
98 |
??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''
|
|
walther@59814
|
99 |
''test''), ORundef, true, true),
|
|
walther@59814
|
100 |
... ctxt: []) ,
|
|
walther@59814
|
101 |
Res ..... NONE)
|
|
walther@59814
|
102 |
--------- ([3], Pbl)--------- Step.do_next \<rightarrow> Add_Given equality (-1 + x = 0)----------------------------------
|
|
walther@59814
|
103 |
========= ([3], Met)========= Step.by_tactic: Apply_Method ["Test","solve_linear"] ==================================
|
|
walther@59814
|
104 |
Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [], e_rls, NONE, ??.empty, ORundef, false, true),
|
|
walther@59814
|
105 |
... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) ,
|
|
walther@59814
|
106 |
Res ..... NONE)
|
|
walther@59814
|
107 |
--------- ([3,1], Frm)--------- Step.do_next \<rightarrow> Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv")----------------------------------
|
|
walther@59814
|
108 |
Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [], e_rls, NONE, ??.empty, ORundef, false, true),
|
|
walther@59814
|
109 |
... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) ,
|
|
walther@59814
|
110 |
Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,L,R,L,R,L,R], e_rls, SOME e_e, x = 0 + -1 * -1, ORundef, true, false),
|
|
walther@59814
|
111 |
... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) )
|
|
walther@59814
|
112 |
========= ([3,1], Frm)========= Step.by_tactic: Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv") ==================================
|
|
walther@59814
|
113 |
Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [], e_rls, NONE, ??.empty, ORundef, false, true),
|
|
walther@59814
|
114 |
... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) ,
|
|
walther@59814
|
115 |
Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,L,R,L,R,L,R], e_rls, SOME e_e, x = 0 + -1 * -1, ORundef, true, true),
|
|
walther@59814
|
116 |
... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) )
|
|
walther@59814
|
117 |
--------- ([3,1], Res)--------- Step.do_next \<rightarrow> Rewrite_Set "Test_simplify"----------------------------------
|
|
walther@59814
|
118 |
Frm ..... (NONE,
|
|
walther@59814
|
119 |
Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,L,R,L,R,R], e_rls, SOME e_e, x = 1, ORundef, true, false),
|
|
walther@59814
|
120 |
... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) )
|
|
walther@59814
|
121 |
========= ([3,1], Res)========= Step.by_tactic: Rewrite_Set "Test_simplify" ==================================
|
|
walther@59814
|
122 |
Frm ..... (NONE,
|
|
walther@59814
|
123 |
Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,L,R,L,R,R], e_rls, SOME e_e, x = 1, ORundef, true, false),
|
|
walther@59814
|
124 |
... ctxt: ["matches (?a = ?b) (-1 + x = 0)"]) )
|
|
walther@59814
|
125 |
--------- ([3,2], Res)--------- Step.do_next \<rightarrow> Check_Postcond ["LINEAR","univariate","equation","test"]----------------------------------
|
|
walther@59814
|
126 |
Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], e_rls, NONE, Subproblem
|
|
walther@59814
|
127 |
(''Test'',
|
|
walther@59814
|
128 |
??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''
|
|
walther@59814
|
129 |
''test''), ORundef, true, true),
|
|
walther@59814
|
130 |
... ctxt: []) ,
|
|
walther@59814
|
131 |
Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], e_rls, NONE, [x = 1], ORundef, true, true),
|
|
walther@59814
|
132 |
... ctxt: ["matches (?a = ?b) (-1 + x = 0)","x = 1"]) )
|
|
walther@59814
|
133 |
========= ([3,2], Res)========= Step.by_tactic: Check_Postcond ["LINEAR","univariate","equation","test"] ==================================
|
|
walther@59814
|
134 |
Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], e_rls, NONE, Subproblem
|
|
walther@59814
|
135 |
(''Test'',
|
|
walther@59814
|
136 |
??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''
|
|
walther@59814
|
137 |
''test''), ORundef, true, true),
|
|
walther@59814
|
138 |
... ctxt: []) ,
|
|
walther@59814
|
139 |
Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], e_rls, NONE, [x = 1], ORundef, true, true),
|
|
walther@59814
|
140 |
... ctxt: ["matches (?a = ?b) (-1 + x = 0)","x = 1"]) )
|
|
walther@59814
|
141 |
--------- ([3], Res)--------- Step.do_next \<rightarrow> Check_elementwise "Assumptions"----------------------------------
|
|
walther@59814
|
142 |
Frm ..... (NONE,
|
|
walther@59814
|
143 |
Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], e_rls, NONE, [x = 1], ORundef, true, false),
|
|
walther@59814
|
144 |
... ctxt: ["matches (?a = ?b) (-1 + x = 0)","x = 1"]) )
|
|
walther@59814
|
145 |
========= ([3], Res)========= Step.by_tactic: Check_elementwise "Assumptions" ==================================
|
|
walther@59814
|
146 |
Frm ..... (NONE,
|
|
walther@59814
|
147 |
Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], e_rls, NONE, [x = 1], ORundef, true, true),
|
|
walther@59814
|
148 |
... ctxt: ["matches (?a = ?b) (-1 + x = 0)","x = 1"]) )
|
|
walther@59814
|
149 |
--------- ([4], Res)--------- Step.do_next \<rightarrow> Check_Postcond ["sqroot-test","univariate","equation","test"]----------------------------------
|
|
walther@59814
|
150 |
Frm ..... (SOME (Pstate ([], [], e_rls, NONE, ??.empty, ORundef, false, false),
|
|
walther@59814
|
151 |
... ctxt: []) ,
|
|
walther@59814
|
152 |
Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], e_rls, NONE, [x = 1], ORundef, true, true),
|
|
walther@59814
|
153 |
... ctxt: ["matches (?a = ?b) (-1 + x = 0)","x = 1"]) )
|
|
walther@59814
|
154 |
========= ([4], Res)========= Step.by_tactic: Check_Postcond ["sqroot-test","univariate","equation","test"] ==================================
|
|
walther@59814
|
155 |
Frm ..... (SOME (Pstate ([], [], e_rls, NONE, ??.empty, ORundef, false, false),
|
|
walther@59814
|
156 |
... ctxt: []) ,
|
|
walther@59814
|
157 |
Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], e_rls, NONE, [x = 1], ORundef, true, true),
|
|
walther@59814
|
158 |
... ctxt: ["matches (?a = ?b) (-1 + x = 0)","x = 1"]) )
|
|
walther@59814
|
159 |
--------- ([], Res)--------- Step.do_next \<rightarrow> input End_Proof'----------------------------------
|
|
walther@59814
|
160 |
========= ([], Res)========= Step.by_tactic: input End_Proof' ==================================
|
|
walther@59814
|
161 |
Frm ..... (SOME (Pstate ([], [], e_rls, NONE, ??.empty, ORundef, false, false),
|
|
walther@59814
|
162 |
... ctxt: []) ,
|
|
walther@59814
|
163 |
Res ..... SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], e_rls, NONE, [x = 1], ORundef, true, true),
|
|
walther@59814
|
164 |
... ctxt: ["matches (?a = ?b) (-1 + x = 0)","x = 1"]) )
|
|
walther@59814
|
165 |
--------- ([], Res)--------- Step.do_next \<rightarrow> input End_Proof'----------------------------------
|
|
walther@59814
|
166 |
*) |