1 (* testexamples for RootratEq, equations mixing fractions and roots
2 WN120314 some complicated equations still are outcommented.
5 "-----------------------------------------------------------------";
6 "table of contents -----------------------------------------------";
7 "-----------------------------------------------------------------";
8 "------------ tests on predicates -------------------------------";
9 "------------ test thm rootrat_equation_left_1 -------------------";
10 "------------ test thm rootrat_equation_left_2 -------------------";
11 "------------ test thm rootrat_equation_right_1 ------------------";
12 "------------ test thm rootrat_equation_right_2 ------------------";
13 "-----------------------------------------------------------------";
14 "-----------------------------------------------------------------";
15 (* Note on ERROR "check_elementwise: no set 1 + sqrt x = 3".
16 this error popped up with this harmless changeset, which
17 (1) triggered ["RootEq", "solve_sq_root_equation"] first time, because wrong '' in
18 (Try (Repeat (Rewrite_Set ''make_rooteq ''))) was found
19 (2) correction ''make_rooteq'' led further to "check_elementwise: no set 1 + sqrt x = 3"
20 Since the changeset seems have nothing todo with these errors, this indicates that
21 (a) either method ["RootEq", "solve_sq_root_equation"] & Co are somewhat indeterministic
22 (b) of this is a case of indeterminism due to something elementary.
25 val thy = @{theory "RootRatEq"};
26 val ctxt = Proof_Context.init_global thy;
28 "------------ tests on predicates -------------------------------";
29 "------------ tests on predicates -------------------------------";
30 "------------ tests on predicates -------------------------------";
31 val t1 = ParseC.parse_test ctxt "(-8 - sqrt(x) + x \<up> 2) is_rootRatAddTerm_in x";
32 val SOME (t,_) = rewrite_set_ ctxt false RootRatEq_prls t1;
33 if (UnparseC.term @{context} t) = "False" then ()
34 else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in";
36 val t1 = ParseC.parse_test ctxt "(1/x) is_rootRatAddTerm_in x";
37 val SOME (t,_) = rewrite_set_ ctxt false RootRatEq_prls t1;
38 if (UnparseC.term @{context} t) = "False" then ()
39 else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in";
41 val t1 = ParseC.parse_test ctxt "(1/sqrt(x)) is_rootRatAddTerm_in x";
42 val SOME (t,_) = rewrite_set_ ctxt false RootRatEq_prls t1;
43 if (UnparseC.term @{context} t) = "False" then ()
44 else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in";
46 val t1 = ParseC.parse_test ctxt "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
47 val SOME (t,_) = rewrite_set_ ctxt false RootRatEq_prls t1;
48 if (UnparseC.term @{context} t) = "True" then ()
49 else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in";
51 val t1 = ParseC.parse_test ctxt "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
52 val SOME (t,_) = rewrite_set_ ctxt false RootRatEq_prls t1;
53 if (UnparseC.term @{context} t) = "True" then ()
54 else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in";
56 val t1 = ParseC.parse_test ctxt "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
57 val SOME (t,_) = rewrite_set_ ctxt false RootRatEq_prls t1;
58 if (UnparseC.term @{context} t) = "True" then ()
59 else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in";
61 val t1 = ParseC.parse_test ctxt "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
62 val SOME (t,_) = rewrite_set_ ctxt false RootRatEq_prls t1;
63 if (UnparseC.term @{context} t) = "True" then ()
64 else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";
66 "------------ test thm rootrat_equation_left_1 -------------------";
67 "------------ test thm rootrat_equation_left_1 -------------------";
68 "------------ test thm rootrat_equation_left_1 -------------------";
70 val fmz = ["equality ( - 2 + 1/(1 - sqrt(x))= (0::real))", "solveFor x", "solutions L"];
71 val (dI',pI',mI') = ("RootRatEq",["univariate", "equation"],["no_met"]);
72 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
73 val (p,_,f,nxt,_,pt) = me nxt p c pt;
74 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
75 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
76 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
77 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
78 val (p,_,f,nxt,_,pt) = me nxt p c pt;
79 (*============ inhibit exn WN120319 ==============================================
80 (*From final Test_Isac.thy we suddenly have
82 nxt = ("Model_Problem", Model_Problem)
84 which we did not investigate further due to the decision to drop the whole type of equation.
86 if f2str f = "1 = (0 - - 2) * (1 + - 1 * sqrt x)" then ()
87 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 a";
88 (*-> Subproblem ("RootRatEq", ["sq", "rootX", "univariate", "equation"])*)
89 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
90 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
91 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
92 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
93 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p''',_,f,nxt,_,pt''') = me nxt p c pt;
95 (*we investigate, why the next step results in Empty_Tac*)
96 f2str f = "1 = 2 * (1 + - 1 * sqrt x)";
97 nxt = ("Rewrite_Set", Rewrite_Set "make_rooteq");
98 (*... these ar the step's arguments; from these we do directly ...*)
99 val SOME t = ParseC.term_opt ctxt "1 = 2 * (1 + - 1 * sqrt x)"
100 val SOME (t, _) = rewrite_set_ thy true make_rooteq t;
101 UnparseC.term @{context} t = "1 = 2 + - 2 * sqrt x";
102 (*... which works; thus error must be in script interpretation*)
104 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
105 val (pt, p) = case Step.by_tactic tac (pt,p) of
106 ("ok", (_, _, ptp)) => ptp;
107 "~~~~~ fun Step.do_next, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
108 val pIopt = get_pblID (pt,ip);
109 ip; (*= ([3, 2], Res)*)
111 pIopt; (*= SOME ["sq", "rootX", "univariate", "equation"]*)
112 member op = [Pbl,Met] p_; (*= false*)
113 "~~~~~ fun do_next, args:"; (*stopped due to strange exn
114 "check_elementwise: no set 1 = 2 + - 2 * sqrt x"*)
116 (*---- 2nd try: we investigate the script ["RootEq", "solve_sq_root_equation"] found via pbl*)
117 val t = ParseC.parse_test @{context} "((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v)";
118 val t = ParseC.parse_test @{context} ("((lhs (1 = 2 * (1 + - 1 * sqrt x))) is_sqrtTerm_in x) |" ^
119 " ((rhs (1 = 2 * (1 + - 1 * sqrt x))) is_sqrtTerm_in x)");
120 val SOME (t, _) = rewrite_set_ thy true rooteq_srls t;
121 UnparseC.term @{context} t = "True | True"; (*...was same in 2002 (NOT "True"); so program seems to take
122 [univariate,equation] and to refine to ["sq", "rootX", "univariate", "equation"] in 2002*)
124 (*(*these are the errors during stepping into the code:*)
125 Step_Solve.do_next (pt,ip); (*check_elementwise: no set 1 = 2 + - 2 * sqrt x: fun mk_set raises
126 this exn in Check_elementwise ONLY ?!?*)
127 Step.do_next p ((pt, e_pos'),[]); (* = ("helpless",*)
130 val (p,_,f,nxt,_,pt) = me nxt p''' c pt''';
131 f2str f = "1 = 2 + - 2 * sqrt x)"; (* <<<-------------- this should be*)
132 fst nxt = "Empty_Tac"; (* <<<-------------- this we have*)
133 (*============ inhibit exn WN120314: stopped due to effort; continue with equ-solver
134 The equation is strange: it calls script ["RootEq", "solve_sq_root_equation"] twice
135 and works differently due to an "if" in that script.
137 if f2str f = "1 = 2 + - 2 * sqrt x" then ()
138 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 b";
139 (*-> Subproblem ("RootRatEq", ["sq", "rootX", "univariate", "equation"]) ?!? the SAME as above*)
140 val (p,_,f,nxt,_,pt) = me nxt p c pt;
141 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
142 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
143 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
144 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
145 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
146 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
147 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
148 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
149 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
150 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
151 if f2str f = "1 = 4 * x" then ()
152 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 c";
153 (*-> Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"])*)
154 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
155 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
156 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
157 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
158 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
159 val (p,_,f,nxt,_,pt) = me nxt p c pt;
160 if f2str f = "1 + -4 * x = 0" then ()
161 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1";
162 (*-> Subproblem ("PolyEq", ["degree_1", "polynomial", "univariate", "equation"])*)
163 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
164 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
165 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
166 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
167 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
168 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
169 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
170 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
171 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
172 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
173 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
174 | _ => error "rootrateq.sml: diff.behav. in - 2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
175 ============ inhibit exn WN120314 ==============================================*)
176 ============ inhibit exn WN120319 ==============================================*)
178 "------------ test thm rootrat_equation_left_2 -------------------";
179 "------------ test thm rootrat_equation_left_2 -------------------";
180 "------------ test thm rootrat_equation_left_2 -------------------";
181 val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x", "solutions L"];
182 val (dI',pI',mI') = ("RootRatEq",["univariate", "equation"],["no_met"]);
184 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
185 val (p,_,f,nxt,_,pt) = me nxt p c pt;
186 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
187 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
188 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
190 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
191 (*-> Subproblem ("RootEq", ["univariate", ...])*)
192 val (p,_,f,nxt,_,pt) = me nxt p c pt;
193 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
194 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
195 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
197 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
199 (*//------------------ ERROR check_elementwise: no set 1 + sqrt x = 3 -----------------------\\* )
200 val (p,_,f,nxt,_,pt) = me nxt p c pt;
201 (*-> Subproblem ("RootEq", ["univariate", ...])*)
202 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
203 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
204 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
206 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
207 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
208 val (p,_,f,nxt,_,pt) = me nxt p c pt;
209 (*-> Subproblem ("RootEq", ["univariate", ...])*)
210 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
211 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
213 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
214 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
215 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
216 val (p,_,f,nxt,_,pt) = me nxt p c pt;
217 ( *\\------------------ ERROR check_elementwise: no set 1 + sqrt x = 3 -----------------------//*)
219 (*============ inhibit exn WN120314 ==============================================
220 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "4 + - 1 * x = 0")) then ()
221 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_2";
222 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
223 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
224 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
225 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
226 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
227 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
228 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
229 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
230 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
231 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
232 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
233 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
234 | _ => error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]";
235 ============ inhibit exn WN120314 ==============================================*)
237 "------------ test thm rootrat_equation_right_1 ------------------";
238 "------------ test thm rootrat_equation_right_1 ------------------";
239 "------------ test thm rootrat_equation_right_1 ------------------";
240 val fmz = ["equality ( 0= - 2 + 1/(1 - sqrt(x)))", "solveFor x", "solutions L"];
241 val (dI',pI',mI') = ("RootRatEq",["univariate", "equation"],["no_met"]);
243 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
244 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
245 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
246 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
247 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
248 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
250 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
251 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
252 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
253 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
254 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
256 (*//------------------ ERROR check_elementwise: no set 1 + sqrt x = 3 -----------------------\\* )
257 val (p,_,f,nxt,_,pt) = me nxt p c pt;
258 val (p,_,f,nxt,_,pt) = me nxt p c pt;
259 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
260 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
261 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
262 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
264 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
265 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
266 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
267 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
268 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
270 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
271 val (p,_,f,nxt,_,pt) = me nxt p c pt;
272 ( *\\------------------ ERROR check_elementwise: no set 1 + sqrt x = 3 -----------------------//*)
274 (*============ inhibit exn WN120314: similar complicated equation, dropped.
275 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "- 1 + 4 * x = 0")) then ()
276 else error "rootrateq.sml: diff.behav.ppoly in rootrat_equation_right_1";
277 val (p,_,f,nxt,_,pt) = me nxt p c pt;
278 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
279 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
280 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
281 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
282 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
283 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
284 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
285 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
286 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
287 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
288 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
289 | _ => error "rootrateq.sml: diff.behav. in - 2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
290 ============ inhibit exn WN120314 ==============================================*)
292 "------------ test thm rootrat_equation_right_2 ------------------";
293 "------------ test thm rootrat_equation_right_2 ------------------";
294 "------------ test thm rootrat_equation_right_2 ------------------";
295 val fmz = ["equality (1 = 3/(1+sqrt(x)))", "solveFor x", "solutions L"];
296 val (dI',pI',mI') = ("RootRatEq",["univariate", "equation"],["no_met"]);
298 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
299 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
300 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
301 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
302 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
303 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
305 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
306 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
307 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
308 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
310 (*//------------------ ERROR rls "make_rooteq " missing in Know_Store.
311 after repair (Try (Repeat (Rewrite_Set ''make_rooteq '')))
312 ------------------ ERROR check_elementwise: no set 1 + sqrt x = 3 -----------------------\\* )
313 (*val (p,_,f,nxt,_,pt) =*) me nxt p c pt;
314 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
316 (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
317 case Step.by_tactic tac (pt, p) of
318 ("ok", (_, _, ptp)) => ptp
319 | ("unsafe-ok", (_, _, ptp)) => ptp
320 | ("not-applicable",_) => (pt, p)
321 | ("end-of-calculation", (_, _, ptp)) => ptp
322 | ("failure", _) => error "sys-error"
323 | _ => error "me: uncovered case Step.by_tactic"
326 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
327 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
328 = (p, ((pt, Pos.e_pos'), []));
329 val pIopt = Ctree.get_pblID (pt, ip);
330 (*if*) ip = ([], Pos.Res) (*else*);
331 val _ = (*case*) tacis (*of*);
332 val SOME _ = (*case*) pIopt (*of*);
334 switch_specify_solve p_ (pt, ip);
335 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
336 (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*else*);
338 LI.do_next (pt, input_pos);
339 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
340 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
341 val thy' = get_obj g_domID pt (par_pblobj pt p);
343 val (_, (ist, ctxt), sc) =
344 LItool.resume_prog (p,p_) pt;
345 "~~~~~ fun resume_prog , args:"; val (thy, (p, p_), pt) = (thy', (p,p_), pt);
346 (*if*) Pos.on_specification (p, p_) (*else*);
347 val (pbl, p', rls') = parent_node pt pos
349 val metID = get_obj g_metID pt p'
350 (*["RootEq", "solve_sq_root_equation"] found for correction, which caused ERROR 2*)
352 (*\\------------------ end ERROR check ------------------------------------------------------//*)
354 val (p,_,f,nxt,_,pt) = me nxt p c pt;
356 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
357 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
358 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
359 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
360 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
362 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
363 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
364 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
365 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
366 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
368 val (p,_,f,nxt,_,pt) = me nxt p c pt;
369 ( *\\------------------ ERROR WN200211 1, 2 -------------------------------------------------//*)
371 (*============ inhibit exn WN120314 ==============================================
372 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "-4 + x = 0")) then ()
373 else error "rootrateq.sml: diff.behav. in rootrat_equation_right_2";
374 val (p,_,f,nxt,_,pt) = me nxt p c pt;
375 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
376 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
377 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
378 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
379 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
380 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
381 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
382 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
383 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
384 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
385 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
386 | _ => error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]";
387 ============ inhibit exn WN120314 ==============================================*)