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