|
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 |
"-----------------------------------------------------------------";
|
|
neuper@41943
|
15 |
|
|
neuper@42393
|
16 |
val thy = @{theory "RootRatEq"};
|
|
neuper@41943
|
17 |
|
|
neuper@42393
|
18 |
"------------ tests on predicates -------------------------------";
|
|
neuper@42393
|
19 |
"------------ tests on predicates -------------------------------";
|
|
neuper@42393
|
20 |
"------------ tests on predicates -------------------------------";
|
|
wneuper@59188
|
21 |
val t1 = (Thm.term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x";
|
|
neuper@42393
|
22 |
val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
|
|
neuper@42393
|
23 |
if (term2str t) = "False" then ()
|
|
neuper@38031
|
24 |
else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
25 |
|
|
wneuper@59188
|
26 |
val t1 = (Thm.term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x";
|
|
neuper@42393
|
27 |
val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
|
|
neuper@42393
|
28 |
if (term2str t) = "False" then ()
|
|
neuper@38031
|
29 |
else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
30 |
|
|
wneuper@59188
|
31 |
val t1 = (Thm.term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x";
|
|
neuper@42393
|
32 |
val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
|
|
neuper@42393
|
33 |
if (term2str t) = "False" then ()
|
|
neuper@38031
|
34 |
else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
35 |
|
|
wneuper@59188
|
36 |
val t1 = (Thm.term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
|
|
neuper@42393
|
37 |
val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
|
|
neuper@42393
|
38 |
if (term2str t) = "True" then ()
|
|
neuper@38031
|
39 |
else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
40 |
|
|
wneuper@59188
|
41 |
val t1 = (Thm.term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
|
|
neuper@42393
|
42 |
val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
|
|
neuper@42393
|
43 |
if (term2str t) = "True" then ()
|
|
neuper@38031
|
44 |
else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
45 |
|
|
wneuper@59188
|
46 |
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
|
47 |
val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
|
|
neuper@42393
|
48 |
if (term2str t) = "True" then ()
|
|
neuper@38031
|
49 |
else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
50 |
|
|
wneuper@59188
|
51 |
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
|
52 |
val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
|
|
neuper@42393
|
53 |
if (term2str t) = "True" then ()
|
|
neuper@38031
|
54 |
else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
55 |
|
|
neuper@42393
|
56 |
"------------ test thm rootrat_equation_left_1 -------------------";
|
|
neuper@42393
|
57 |
"------------ test thm rootrat_equation_left_1 -------------------";
|
|
neuper@42393
|
58 |
"------------ test thm rootrat_equation_left_1 -------------------";
|
|
neuper@42393
|
59 |
val c = [];
|
|
neuper@42393
|
60 |
val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= (0::real))", "solveFor x","solutions L"];
|
|
neuper@37991
|
61 |
val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
|
|
neuper@37906
|
62 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@37906
|
63 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
64 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
65 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
66 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
67 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@42398
|
68 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@42398
|
69 |
(*============ inhibit exn WN120319 ==============================================
|
|
neuper@42398
|
70 |
(*From final Test_Isac.thy we suddenly have
|
|
neuper@42398
|
71 |
|
|
neuper@42398
|
72 |
nxt = ("Model_Problem", Model_Problem)
|
|
neuper@42398
|
73 |
|
|
neuper@42398
|
74 |
which we did not investigate further due to the decision to drop the whole type of equation.
|
|
neuper@42398
|
75 |
*)
|
|
neuper@42393
|
76 |
if f2str f = "1 = (0 - -2) * (1 + -1 * sqrt x)" then ()
|
|
neuper@42393
|
77 |
else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 a";
|
|
neuper@42393
|
78 |
(*-> Subproblem ("RootRatEq", ["sq", "root'", "univariate", "equation"])*)
|
|
neuper@42393
|
79 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@42393
|
80 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@42393
|
81 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@42393
|
82 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@42393
|
83 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p''',_,f,nxt,_,pt''') = me nxt p c pt;
|
|
neuper@42393
|
84 |
|
|
neuper@42393
|
85 |
(*we investigate, why the next step results in Empty_Tac*)
|
|
neuper@42393
|
86 |
f2str f = "1 = 2 * (1 + -1 * sqrt x)";
|
|
neuper@42393
|
87 |
nxt = ("Rewrite_Set", Rewrite_Set "make_rooteq");
|
|
neuper@42393
|
88 |
(*... these ar the step's arguments; from these we do directly ...*)
|
|
neuper@42393
|
89 |
val SOME t = parseNEW ctxt "1 = 2 * (1 + -1 * sqrt x)"
|
|
neuper@42393
|
90 |
val SOME (t, _) = rewrite_set_ thy true make_rooteq t;
|
|
neuper@42393
|
91 |
term2str t = "1 = 2 + -2 * sqrt x";
|
|
neuper@42393
|
92 |
(*... which works; thus error must be in script interpretation*)
|
|
neuper@42393
|
93 |
|
|
wneuper@59279
|
94 |
"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
|
|
neuper@42393
|
95 |
val (pt, p) = case locatetac tac (pt,p) of
|
|
neuper@42393
|
96 |
("ok", (_, _, ptp)) => ptp;
|
|
neuper@42393
|
97 |
"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
|
|
neuper@42393
|
98 |
val pIopt = get_pblID (pt,ip);
|
|
neuper@42393
|
99 |
ip; (*= ([3, 2], Res)*)
|
|
neuper@42393
|
100 |
tacis; (*= []*)
|
|
neuper@42393
|
101 |
pIopt; (*= SOME ["sq", "root'", "univariate", "equation"]*)
|
|
neuper@42393
|
102 |
member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
|
|
neuper@42393
|
103 |
"~~~~~ fun nxt_solve_, args:"; (*stopped due to strange exn
|
|
neuper@42393
|
104 |
"check_elementwise: no set 1 = 2 + -2 * sqrt x"*)
|
|
neuper@42393
|
105 |
|
|
neuper@42393
|
106 |
(*---- 2nd try: we investigate the script ["RootEq","solve_sq_root_equation"] found via pbl*)
|
|
neuper@42393
|
107 |
val t = str2term "((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v)";
|
|
neuper@42393
|
108 |
val t = str2term ("((lhs (1 = 2 * (1 + -1 * sqrt x))) is_sqrtTerm_in x) |" ^
|
|
neuper@42393
|
109 |
" ((rhs (1 = 2 * (1 + -1 * sqrt x))) is_sqrtTerm_in x)");
|
|
neuper@42393
|
110 |
val SOME (t, _) = rewrite_set_ thy true rooteq_srls t;
|
|
neuper@42393
|
111 |
term2str t = "True | True"; (*...was same in 2002 (NOT "True"); so program seems to take
|
|
neuper@42393
|
112 |
[univariate,equation] and to refine to ["sq", "root'", "univariate", "equation"] in 2002*)
|
|
neuper@42393
|
113 |
|
|
neuper@42393
|
114 |
(*(*these are the errors during stepping into the code:*)
|
|
neuper@42393
|
115 |
nxt_solve_ (pt,ip); (*check_elementwise: no set 1 = 2 + -2 * sqrt x: fun mk_set raises
|
|
neuper@42393
|
116 |
this exn in Check_elementwise ONLY ?!?*)
|
|
neuper@42393
|
117 |
step p ((pt, e_pos'),[]); (* = ("helpless",*)
|
|
neuper@42393
|
118 |
*)
|
|
neuper@42393
|
119 |
|
|
neuper@42393
|
120 |
val (p,_,f,nxt,_,pt) = me nxt p''' c pt''';
|
|
neuper@42393
|
121 |
f2str f = "1 = 2 + -2 * sqrt x)"; (* <<<-------------- this should be*)
|
|
neuper@42393
|
122 |
fst nxt = "Empty_Tac"; (* <<<-------------- this we have*)
|
|
neuper@42393
|
123 |
(*============ inhibit exn WN120314: stopped due to effort; continue with equ-solver
|
|
neuper@42393
|
124 |
The equation is strange: it calls script ["RootEq","solve_sq_root_equation"] twice
|
|
neuper@42393
|
125 |
and works differently due to an "if" in that script.
|
|
neuper@42393
|
126 |
|
|
neuper@42393
|
127 |
if f2str f = "1 = 2 + -2 * sqrt x" then ()
|
|
neuper@42393
|
128 |
else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 b";
|
|
neuper@42393
|
129 |
(*-> Subproblem ("RootRatEq", ["sq", "root'", "univariate", "equation"]) ?!? the SAME as above*)
|
|
neuper@42393
|
130 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@42393
|
131 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@42393
|
132 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@42393
|
133 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@42393
|
134 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@42393
|
135 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@42393
|
136 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@42393
|
137 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@42393
|
138 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@42393
|
139 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@42393
|
140 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@42393
|
141 |
if f2str f = "1 = 4 * x" then ()
|
|
neuper@42393
|
142 |
else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 c";
|
|
neuper@42393
|
143 |
(*-> Subproblem ("PolyEq", ["normalize", "polynomial", "univariate", "equation"])*)
|
|
neuper@37906
|
144 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
145 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
146 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
147 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
148 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
149 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@42393
|
150 |
if f2str f = "1 + -4 * x = 0" then ()
|
|
neuper@38031
|
151 |
else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1";
|
|
neuper@42393
|
152 |
(*-> Subproblem ("PolyEq", ["degree_1", "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; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
159 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
160 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
161 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
|
|
neuper@38031
|
164 |
| _ => error "rootrateq.sml: diff.behav. in -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
|
|
neuper@42393
|
165 |
============ inhibit exn WN120314 ==============================================*)
|
|
neuper@42398
|
166 |
============ inhibit exn WN120319 ==============================================*)
|
|
neuper@37906
|
167 |
|
|
neuper@42393
|
168 |
"------------ test thm rootrat_equation_left_2 -------------------";
|
|
neuper@42393
|
169 |
"------------ test thm rootrat_equation_left_2 -------------------";
|
|
neuper@42393
|
170 |
"------------ test thm rootrat_equation_left_2 -------------------";
|
|
neuper@37906
|
171 |
val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x","solutions L"];
|
|
neuper@37991
|
172 |
val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
|
|
neuper@37906
|
173 |
|
|
neuper@37906
|
174 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@37906
|
175 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
176 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
177 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
178 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
179 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37991
|
180 |
(*-> Subproblem ("RootEq", ["univariate", ...])*)
|
|
neuper@37906
|
181 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
182 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
183 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
184 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; 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;
|
|
neuper@37991
|
187 |
(*-> Subproblem ("RootEq", ["univariate", ...])*)
|
|
neuper@37906
|
188 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
189 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
190 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
191 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; 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;
|
|
neuper@37991
|
194 |
(*-> Subproblem ("RootEq", ["univariate", ...])*)
|
|
neuper@37906
|
195 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
196 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
197 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
198 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
199 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
200 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@42393
|
201 |
(*============ inhibit exn WN120314 ==============================================
|
|
neuper@37906
|
202 |
if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "4 + -1 * x = 0")) then ()
|
|
neuper@38031
|
203 |
else error "rootrateq.sml: diff.behav. in rootrat_equation_left_2";
|
|
neuper@37991
|
204 |
(*-> Subproblem ("PolyEq", ["polynomial", ...])*)
|
|
neuper@37906
|
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; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
208 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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;
|
|
neuper@37906
|
211 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
|
|
neuper@38031
|
216 |
| _ => error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]";
|
|
neuper@42393
|
217 |
============ inhibit exn WN120314 ==============================================*)
|
|
neuper@37906
|
218 |
|
|
neuper@42393
|
219 |
"------------ test thm rootrat_equation_right_1 ------------------";
|
|
neuper@42393
|
220 |
"------------ test thm rootrat_equation_right_1 ------------------";
|
|
neuper@42393
|
221 |
"------------ test thm rootrat_equation_right_1 ------------------";
|
|
neuper@37906
|
222 |
val fmz = ["equality ( 0= -2 + 1/(1 - sqrt(x)))", "solveFor x","solutions L"];
|
|
neuper@37991
|
223 |
val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
|
|
neuper@37906
|
224 |
|
|
neuper@37906
|
225 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
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;
|
|
neuper@37906
|
233 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
234 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
235 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
236 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
237 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
238 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
239 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
240 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
241 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
242 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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;
|
|
neuper@42393
|
248 |
(*============ inhibit exn WN120314: similar complicated equation, dropped.
|
|
neuper@37906
|
249 |
if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-1 + 4 * x = 0")) then ()
|
|
neuper@38031
|
250 |
else error "rootrateq.sml: diff.behav.ppoly in rootrat_equation_right_1";
|
|
neuper@37906
|
251 |
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;
|
|
neuper@37906
|
255 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
256 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
257 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; 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;
|
|
neuper@37906
|
262 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
|
|
neuper@38031
|
263 |
| _ => error "rootrateq.sml: diff.behav. in -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
|
|
neuper@42393
|
264 |
============ inhibit exn WN120314 ==============================================*)
|
|
neuper@37906
|
265 |
|
|
neuper@42393
|
266 |
"------------ test thm rootrat_equation_right_2 ------------------";
|
|
neuper@42393
|
267 |
"------------ test thm rootrat_equation_right_2 ------------------";
|
|
neuper@42393
|
268 |
"------------ test thm rootrat_equation_right_2 ------------------";
|
|
neuper@37906
|
269 |
val fmz = ["equality (1 = 3/(1+sqrt(x)))", "solveFor x","solutions L"];
|
|
neuper@37991
|
270 |
val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
|
|
neuper@37906
|
271 |
|
|
neuper@37906
|
272 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@37906
|
273 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
274 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
275 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
276 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; 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 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
288 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
289 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
290 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
291 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
292 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
293 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@42393
|
294 |
(*============ inhibit exn WN120314 ==============================================
|
|
neuper@37906
|
295 |
if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-4 + x = 0")) then ()
|
|
neuper@38031
|
296 |
else error "rootrateq.sml: diff.behav. in rootrat_equation_right_2";
|
|
neuper@37906
|
297 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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;
|
|
neuper@37906
|
303 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
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;
|
|
neuper@37906
|
308 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
|
|
neuper@38031
|
309 |
| _ => error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]";
|
|
neuper@42393
|
310 |
============ inhibit exn WN120314 ==============================================*)
|
|
neuper@42393
|
311 |
|