|
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@59803
|
22 |
(b) of this is a case of indeterminism due to "handle _" or something similar elementary.
|
|
neuper@41943
|
23 |
|
|
walther@59803
|
24 |
*)
|
|
neuper@42393
|
25 |
val thy = @{theory "RootRatEq"};
|
|
neuper@41943
|
26 |
|
|
neuper@42393
|
27 |
"------------ tests on predicates -------------------------------";
|
|
neuper@42393
|
28 |
"------------ tests on predicates -------------------------------";
|
|
neuper@42393
|
29 |
"------------ tests on predicates -------------------------------";
|
|
wneuper@59188
|
30 |
val t1 = (Thm.term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x";
|
|
neuper@42393
|
31 |
val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
|
|
neuper@42393
|
32 |
if (term2str t) = "False" then ()
|
|
neuper@38031
|
33 |
else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
34 |
|
|
wneuper@59188
|
35 |
val t1 = (Thm.term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x";
|
|
neuper@42393
|
36 |
val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
|
|
neuper@42393
|
37 |
if (term2str t) = "False" then ()
|
|
neuper@38031
|
38 |
else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
39 |
|
|
wneuper@59188
|
40 |
val t1 = (Thm.term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x";
|
|
neuper@42393
|
41 |
val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
|
|
neuper@42393
|
42 |
if (term2str t) = "False" then ()
|
|
neuper@38031
|
43 |
else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
44 |
|
|
wneuper@59188
|
45 |
val t1 = (Thm.term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
|
|
neuper@42393
|
46 |
val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
|
|
neuper@42393
|
47 |
if (term2str t) = "True" then ()
|
|
neuper@38031
|
48 |
else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
49 |
|
|
wneuper@59188
|
50 |
val t1 = (Thm.term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
|
|
neuper@42393
|
51 |
val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
|
|
neuper@42393
|
52 |
if (term2str t) = "True" then ()
|
|
neuper@38031
|
53 |
else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
54 |
|
|
wneuper@59188
|
55 |
val t1 = (Thm.term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
|
|
neuper@42393
|
56 |
val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
|
|
neuper@42393
|
57 |
if (term2str t) = "True" then ()
|
|
neuper@38031
|
58 |
else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
59 |
|
|
wneuper@59188
|
60 |
val t1 = (Thm.term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
|
|
neuper@42393
|
61 |
val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
|
|
neuper@42393
|
62 |
if (term2str t) = "True" then ()
|
|
neuper@38031
|
63 |
else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
64 |
|
|
neuper@42393
|
65 |
"------------ test thm rootrat_equation_left_1 -------------------";
|
|
neuper@42393
|
66 |
"------------ test thm rootrat_equation_left_1 -------------------";
|
|
neuper@42393
|
67 |
"------------ test thm rootrat_equation_left_1 -------------------";
|
|
neuper@42393
|
68 |
val c = [];
|
|
neuper@42393
|
69 |
val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= (0::real))", "solveFor x","solutions L"];
|
|
neuper@37991
|
70 |
val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
|
|
neuper@37906
|
71 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@37906
|
72 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
73 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; 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@42398
|
77 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@42398
|
78 |
(*============ inhibit exn WN120319 ==============================================
|
|
neuper@42398
|
79 |
(*From final Test_Isac.thy we suddenly have
|
|
neuper@42398
|
80 |
|
|
neuper@42398
|
81 |
nxt = ("Model_Problem", Model_Problem)
|
|
neuper@42398
|
82 |
|
|
neuper@42398
|
83 |
which we did not investigate further due to the decision to drop the whole type of equation.
|
|
neuper@42398
|
84 |
*)
|
|
neuper@42393
|
85 |
if f2str f = "1 = (0 - -2) * (1 + -1 * sqrt x)" then ()
|
|
neuper@42393
|
86 |
else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 a";
|
|
wneuper@59489
|
87 |
(*-> Subproblem ("RootRatEq", ["sq", "rootX", "univariate", "equation"])*)
|
|
neuper@42393
|
88 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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 |
|
|
neuper@42393
|
94 |
(*we investigate, why the next step results in Empty_Tac*)
|
|
neuper@42393
|
95 |
f2str f = "1 = 2 * (1 + -1 * sqrt x)";
|
|
neuper@42393
|
96 |
nxt = ("Rewrite_Set", Rewrite_Set "make_rooteq");
|
|
neuper@42393
|
97 |
(*... these ar the step's arguments; from these we do directly ...*)
|
|
neuper@42393
|
98 |
val SOME t = parseNEW ctxt "1 = 2 * (1 + -1 * sqrt x)"
|
|
neuper@42393
|
99 |
val SOME (t, _) = rewrite_set_ thy true make_rooteq t;
|
|
neuper@42393
|
100 |
term2str t = "1 = 2 + -2 * sqrt x";
|
|
neuper@42393
|
101 |
(*... which works; thus error must be in script interpretation*)
|
|
neuper@42393
|
102 |
|
|
walther@59749
|
103 |
"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
|
|
neuper@42393
|
104 |
val (pt, p) = case locatetac tac (pt,p) of
|
|
neuper@42393
|
105 |
("ok", (_, _, ptp)) => ptp;
|
|
walther@59765
|
106 |
"~~~~~ fun Step.do_next, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
|
|
neuper@42393
|
107 |
val pIopt = get_pblID (pt,ip);
|
|
neuper@42393
|
108 |
ip; (*= ([3, 2], Res)*)
|
|
neuper@42393
|
109 |
tacis; (*= []*)
|
|
wneuper@59489
|
110 |
pIopt; (*= SOME ["sq", "rootX", "univariate", "equation"]*)
|
|
neuper@42393
|
111 |
member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
|
|
walther@59760
|
112 |
"~~~~~ fun do_next, args:"; (*stopped due to strange exn
|
|
neuper@42393
|
113 |
"check_elementwise: no set 1 = 2 + -2 * sqrt x"*)
|
|
neuper@42393
|
114 |
|
|
neuper@42393
|
115 |
(*---- 2nd try: we investigate the script ["RootEq","solve_sq_root_equation"] found via pbl*)
|
|
neuper@42393
|
116 |
val t = str2term "((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v)";
|
|
neuper@42393
|
117 |
val t = str2term ("((lhs (1 = 2 * (1 + -1 * sqrt x))) is_sqrtTerm_in x) |" ^
|
|
neuper@42393
|
118 |
" ((rhs (1 = 2 * (1 + -1 * sqrt x))) is_sqrtTerm_in x)");
|
|
neuper@42393
|
119 |
val SOME (t, _) = rewrite_set_ thy true rooteq_srls t;
|
|
neuper@42393
|
120 |
term2str t = "True | True"; (*...was same in 2002 (NOT "True"); so program seems to take
|
|
wneuper@59489
|
121 |
[univariate,equation] and to refine to ["sq", "rootX", "univariate", "equation"] in 2002*)
|
|
neuper@42393
|
122 |
|
|
neuper@42393
|
123 |
(*(*these are the errors during stepping into the code:*)
|
|
walther@59760
|
124 |
Step_Solve.do_next (pt,ip); (*check_elementwise: no set 1 = 2 + -2 * sqrt x: fun mk_set raises
|
|
neuper@42393
|
125 |
this exn in Check_elementwise ONLY ?!?*)
|
|
walther@59765
|
126 |
Step.do_next p ((pt, e_pos'),[]); (* = ("helpless",*)
|
|
neuper@42393
|
127 |
*)
|
|
neuper@42393
|
128 |
|
|
neuper@42393
|
129 |
val (p,_,f,nxt,_,pt) = me nxt p''' c pt''';
|
|
neuper@42393
|
130 |
f2str f = "1 = 2 + -2 * sqrt x)"; (* <<<-------------- this should be*)
|
|
neuper@42393
|
131 |
fst nxt = "Empty_Tac"; (* <<<-------------- this we have*)
|
|
neuper@42393
|
132 |
(*============ inhibit exn WN120314: stopped due to effort; continue with equ-solver
|
|
neuper@42393
|
133 |
The equation is strange: it calls script ["RootEq","solve_sq_root_equation"] twice
|
|
neuper@42393
|
134 |
and works differently due to an "if" in that script.
|
|
neuper@42393
|
135 |
|
|
neuper@42393
|
136 |
if f2str f = "1 = 2 + -2 * sqrt x" then ()
|
|
neuper@42393
|
137 |
else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 b";
|
|
wneuper@59489
|
138 |
(*-> Subproblem ("RootRatEq", ["sq", "rootX", "univariate", "equation"]) ?!? the SAME as above*)
|
|
neuper@42393
|
139 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@42393
|
140 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
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 |
if f2str f = "1 = 4 * x" then ()
|
|
neuper@42393
|
151 |
else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 c";
|
|
wneuper@59367
|
152 |
(*-> Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"])*)
|
|
neuper@37906
|
153 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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;
|
|
neuper@42393
|
159 |
if f2str f = "1 + -4 * x = 0" then ()
|
|
neuper@38031
|
160 |
else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1";
|
|
neuper@42393
|
161 |
(*-> Subproblem ("PolyEq", ["degree_1", "polynomial", "univariate", "equation"])*)
|
|
neuper@37906
|
162 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
|
|
neuper@38031
|
173 |
| _ => error "rootrateq.sml: diff.behav. in -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
|
|
neuper@42393
|
174 |
============ inhibit exn WN120314 ==============================================*)
|
|
neuper@42398
|
175 |
============ inhibit exn WN120319 ==============================================*)
|
|
neuper@37906
|
176 |
|
|
neuper@42393
|
177 |
"------------ test thm rootrat_equation_left_2 -------------------";
|
|
neuper@42393
|
178 |
"------------ test thm rootrat_equation_left_2 -------------------";
|
|
neuper@42393
|
179 |
"------------ test thm rootrat_equation_left_2 -------------------";
|
|
neuper@37906
|
180 |
val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x","solutions L"];
|
|
neuper@37991
|
181 |
val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
|
|
neuper@37906
|
182 |
|
|
neuper@37906
|
183 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@37906
|
184 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
185 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; 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;
|
|
walther@59803
|
188 |
(*^^^ 10 *)
|
|
neuper@37906
|
189 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37991
|
190 |
(*-> Subproblem ("RootEq", ["univariate", ...])*)
|
|
neuper@37906
|
191 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
192 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; 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;
|
|
walther@59803
|
195 |
(*^^^ 20 *)
|
|
walther@59803
|
196 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
walther@59803
|
197 |
|
|
walther@59803
|
198 |
(*//------------------ ERROR check_elementwise: no set 1 + sqrt x = 3 -----------------------\\* )
|
|
walther@59803
|
199 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
walther@59803
|
200 |
(*-> Subproblem ("RootEq", ["univariate", ...])*)
|
|
walther@59803
|
201 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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 |
(*^^^ 30 *)
|
|
walther@59803
|
205 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
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;
|
|
neuper@37991
|
208 |
(*-> Subproblem ("RootEq", ["univariate", ...])*)
|
|
neuper@37906
|
209 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
210 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
walther@59803
|
211 |
(*^^^ 40 *)
|
|
neuper@37906
|
212 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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;
|
|
walther@59803
|
216 |
( *\\------------------ ERROR check_elementwise: no set 1 + sqrt x = 3 -----------------------//*)
|
|
walther@59803
|
217 |
|
|
neuper@42393
|
218 |
(*============ inhibit exn WN120314 ==============================================
|
|
neuper@37906
|
219 |
if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "4 + -1 * x = 0")) then ()
|
|
neuper@38031
|
220 |
else error "rootrateq.sml: diff.behav. in rootrat_equation_left_2";
|
|
neuper@37991
|
221 |
(*-> Subproblem ("PolyEq", ["polynomial", ...])*)
|
|
neuper@37906
|
222 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
|
|
neuper@38031
|
233 |
| _ => error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]";
|
|
neuper@42393
|
234 |
============ inhibit exn WN120314 ==============================================*)
|
|
neuper@37906
|
235 |
|
|
neuper@42393
|
236 |
"------------ test thm rootrat_equation_right_1 ------------------";
|
|
neuper@42393
|
237 |
"------------ test thm rootrat_equation_right_1 ------------------";
|
|
neuper@42393
|
238 |
"------------ test thm rootrat_equation_right_1 ------------------";
|
|
neuper@37906
|
239 |
val fmz = ["equality ( 0= -2 + 1/(1 - sqrt(x)))", "solveFor x","solutions L"];
|
|
neuper@37991
|
240 |
val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
|
|
neuper@37906
|
241 |
|
|
neuper@37906
|
242 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@37906
|
243 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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;
|
|
walther@59803
|
248 |
(*^^^ 10 *)
|
|
neuper@37906
|
249 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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;
|
|
walther@59803
|
254 |
(*^^^ 20 *)
|
|
walther@59803
|
255 |
(*//------------------ ERROR check_elementwise: no set 1 + sqrt x = 3 -----------------------\\* )
|
|
walther@59803
|
256 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
walther@59803
|
257 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
258 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; 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;
|
|
walther@59803
|
262 |
(*^^^ 30 *)
|
|
neuper@37906
|
263 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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;
|
|
walther@59803
|
268 |
(*^^^ 40 *)
|
|
neuper@37906
|
269 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
270 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
walther@59803
|
271 |
( *\\------------------ ERROR check_elementwise: no set 1 + sqrt x = 3 -----------------------//*)
|
|
walther@59803
|
272 |
|
|
neuper@42393
|
273 |
(*============ inhibit exn WN120314: similar complicated equation, dropped.
|
|
neuper@37906
|
274 |
if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-1 + 4 * x = 0")) then ()
|
|
neuper@38031
|
275 |
else error "rootrateq.sml: diff.behav.ppoly in rootrat_equation_right_1";
|
|
neuper@37906
|
276 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
277 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; 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 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
|
|
neuper@38031
|
288 |
| _ => error "rootrateq.sml: diff.behav. in -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
|
|
neuper@42393
|
289 |
============ inhibit exn WN120314 ==============================================*)
|
|
neuper@37906
|
290 |
|
|
neuper@42393
|
291 |
"------------ test thm rootrat_equation_right_2 ------------------";
|
|
neuper@42393
|
292 |
"------------ test thm rootrat_equation_right_2 ------------------";
|
|
neuper@42393
|
293 |
"------------ test thm rootrat_equation_right_2 ------------------";
|
|
neuper@37906
|
294 |
val fmz = ["equality (1 = 3/(1+sqrt(x)))", "solveFor x","solutions L"];
|
|
neuper@37991
|
295 |
val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
|
|
neuper@37906
|
296 |
|
|
neuper@37906
|
297 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@37906
|
298 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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;
|
|
walther@59803
|
303 |
(*^^^ 10 *)
|
|
neuper@37906
|
304 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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;
|
|
walther@59803
|
308 |
|
|
walther@59803
|
309 |
(*//------------------ ERROR rls "make_rooteq " missing in KEStore.
|
|
walther@59803
|
310 |
after repair (Try (Repeat (Rewrite_Set ''make_rooteq '')))
|
|
walther@59803
|
311 |
------------------ ERROR check_elementwise: no set 1 + sqrt x = 3 -----------------------\\* )
|
|
walther@59803
|
312 |
(*val (p,_,f,nxt,_,pt) =*) me nxt p c pt;
|
|
walther@59803
|
313 |
"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
|
|
walther@59803
|
314 |
val (pt, p) =
|
|
walther@59803
|
315 |
(*locatetac is here for testing by me; do_next would suffice in me*)
|
|
walther@59803
|
316 |
case locatetac tac (pt, p) of
|
|
walther@59803
|
317 |
("ok", (_, _, ptp)) => ptp
|
|
walther@59803
|
318 |
| ("unsafe-ok", (_, _, ptp)) => ptp
|
|
walther@59803
|
319 |
| ("not-applicable",_) => (pt, p)
|
|
walther@59803
|
320 |
| ("end-of-calculation", (_, _, ptp)) => ptp
|
|
walther@59803
|
321 |
| ("failure", _) => error "sys-error"
|
|
walther@59803
|
322 |
| _ => error "me: uncovered case locatetac"
|
|
walther@59803
|
323 |
|
|
walther@59803
|
324 |
(*case*)
|
|
walther@59803
|
325 |
Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
|
|
walther@59803
|
326 |
"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
|
|
walther@59803
|
327 |
= (p, ((pt, Pos.e_pos'), []));
|
|
walther@59803
|
328 |
val pIopt = Ctree.get_pblID (pt, ip);
|
|
walther@59803
|
329 |
(*if*) ip = ([], Pos.Res) (*else*);
|
|
walther@59803
|
330 |
val _ = (*case*) tacis (*of*);
|
|
walther@59803
|
331 |
val SOME _ = (*case*) pIopt (*of*);
|
|
walther@59803
|
332 |
|
|
walther@59803
|
333 |
switch_specify_solve p_ (pt, ip);
|
|
walther@59803
|
334 |
"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
|
|
walther@59803
|
335 |
(*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*else*);
|
|
walther@59803
|
336 |
|
|
walther@59803
|
337 |
LI.do_next (pt, input_pos);
|
|
walther@59803
|
338 |
"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
|
|
walther@59803
|
339 |
(*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
|
|
walther@59803
|
340 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
|
walther@59803
|
341 |
|
|
walther@59803
|
342 |
val (_, (ist, ctxt), sc) =
|
|
walther@59803
|
343 |
LItool.from_pblobj_or_detail' thy' (p,p_) pt;
|
|
walther@59803
|
344 |
"~~~~~ fun from_pblobj_or_detail' , args:"; val (thy, (p, p_), pt) = (thy', (p,p_), pt);
|
|
walther@59803
|
345 |
(*if*) Pos.on_specification p_ (*else*);
|
|
walther@59803
|
346 |
val (pbl, p', rls') = par_pbl_det pt p
|
|
walther@59803
|
347 |
(*if*) pbl (*then*);
|
|
walther@59803
|
348 |
val metID = get_obj g_metID pt p'
|
|
walther@59803
|
349 |
(*["RootEq", "solve_sq_root_equation"] found for correction, which caused ERROR 2*)
|
|
walther@59803
|
350 |
|
|
walther@59803
|
351 |
(*\\------------------ end ERROR check ------------------------------------------------------//*)
|
|
walther@59803
|
352 |
|
|
walther@59803
|
353 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
walther@59803
|
354 |
(*^^^ 20 *)
|
|
neuper@37906
|
355 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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;
|
|
walther@59803
|
360 |
(*^^^ 30 *)
|
|
neuper@37906
|
361 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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;
|
|
walther@59803
|
366 |
(*^^^ 40 *)
|
|
neuper@37906
|
367 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
walther@59803
|
368 |
( *\\------------------ ERROR WN200211 1, 2 -------------------------------------------------//*)
|
|
walther@59803
|
369 |
|
|
neuper@42393
|
370 |
(*============ inhibit exn WN120314 ==============================================
|
|
neuper@37906
|
371 |
if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-4 + x = 0")) then ()
|
|
neuper@38031
|
372 |
else error "rootrateq.sml: diff.behav. in rootrat_equation_right_2";
|
|
neuper@37906
|
373 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
374 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; 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 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
|
|
neuper@38031
|
385 |
| _ => error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]";
|
|
neuper@42393
|
386 |
============ inhibit exn WN120314 ==============================================*)
|
|
neuper@42393
|
387 |
|