walther@60389
|
1 |
(* Title: Knowledge/polyeq-1.sml
|
walther@59627
|
2 |
testexamples for PolyEq, poynomial equations and equational systems
|
walther@59627
|
3 |
Author: Richard Lang 2003
|
walther@59627
|
4 |
(c) due to copyright terms
|
walther@60393
|
5 |
|
walther@60393
|
6 |
Separation into polyeq-1.sml and polyeq-1a.sml due to
|
walther@59627
|
7 |
*)
|
walther@59627
|
8 |
|
walther@59627
|
9 |
"-----------------------------------------------------------------";
|
walther@59627
|
10 |
"table of contents -----------------------------------------------";
|
walther@59627
|
11 |
"-----------------------------------------------------------------";
|
walther@60393
|
12 |
"------ polyeq-1.sml ---------------------------------------------";
|
walther@59627
|
13 |
"----------- tests on predicates in problems ---------------------";
|
walther@59627
|
14 |
"----------- test matching problems ------------------------------";
|
walther@59847
|
15 |
"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
|
walther@60342
|
16 |
"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
|
walther@59847
|
17 |
"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
|
walther@59627
|
18 |
"----------- lin.eq degree_0 -------------------------------------";
|
walther@59627
|
19 |
"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
|
walther@60329
|
20 |
"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
|
walther@60329
|
21 |
"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
|
walther@60329
|
22 |
"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
|
walther@60242
|
23 |
"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
|
walther@60329
|
24 |
"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
|
walther@60393
|
25 |
"------ polyeq- 2.sml ---------------------------------------------";
|
walther@60242
|
26 |
"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
|
walther@60242
|
27 |
"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
|
walther@60242
|
28 |
"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
|
walther@60242
|
29 |
"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
|
walther@60242
|
30 |
"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
|
walther@60242
|
31 |
"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
|
walther@60329
|
32 |
"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
|
walther@60329
|
33 |
"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
|
walther@60242
|
34 |
"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
|
walther@60242
|
35 |
"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
|
walther@60242
|
36 |
"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
|
walther@60329
|
37 |
"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
|
walther@59627
|
38 |
"-----------------------------------------------------------------";
|
walther@60329
|
39 |
"------ polyeq- 2.sml ---------------------------------------------";
|
walther@60242
|
40 |
"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
|
walther@60242
|
41 |
"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
|
walther@60329
|
42 |
"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
|
walther@60329
|
43 |
"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
|
walther@60242
|
44 |
"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
|
walther@59627
|
45 |
"----------- rls make_polynomial_in ------------------------------";
|
walther@59627
|
46 |
"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
|
walther@59627
|
47 |
"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
|
walther@59627
|
48 |
"-----------------------------------------------------------------";
|
walther@59627
|
49 |
"-----------------------------------------------------------------";
|
walther@59627
|
50 |
|
walther@59627
|
51 |
"----------- tests on predicates in problems ---------------------";
|
walther@59627
|
52 |
"----------- tests on predicates in problems ---------------------";
|
walther@59627
|
53 |
"----------- tests on predicates in problems ---------------------";
|
walther@60393
|
54 |
val thy = @{theory};
|
walther@60342
|
55 |
Rewrite.trace_on:=false; (*true false*)
|
walther@60330
|
56 |
|
walther@60340
|
57 |
val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
|
walther@59627
|
58 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
|
walther@60342
|
59 |
if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()
|
walther@59627
|
60 |
else error "polyeq.sml: diff.behav. in lhs";
|
walther@59627
|
61 |
|
walther@60340
|
62 |
val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
|
walther@59627
|
63 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
|
walther@59868
|
64 |
if (UnparseC.term t) = "True" then ()
|
walther@59627
|
65 |
else error "polyeq.sml: diff.behav. 1 in is_expended_in";
|
walther@59627
|
66 |
|
walther@60340
|
67 |
val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x";
|
walther@59627
|
68 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
|
walther@59868
|
69 |
if (UnparseC.term t) = "False" then ()
|
walther@59627
|
70 |
else error "polyeq.sml: diff.behav. 2 in is_poly_in";
|
walther@59627
|
71 |
|
walther@60340
|
72 |
val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
|
walther@59627
|
73 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
|
walther@59868
|
74 |
if (UnparseC.term t) = "True" then ()
|
walther@59627
|
75 |
else error "polyeq.sml: diff.behav. 3 in is_poly_in";
|
walther@59627
|
76 |
|
walther@60340
|
77 |
val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
|
walther@59627
|
78 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
|
walther@59868
|
79 |
if (UnparseC.term t) = "True" then ()
|
walther@59627
|
80 |
else error "polyeq.sml: diff.behav. 4 in is_expended_in";
|
walther@59627
|
81 |
|
walther@60340
|
82 |
val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
|
walther@59627
|
83 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
|
walther@59868
|
84 |
if (UnparseC.term t) = "True" then ()
|
walther@59627
|
85 |
else error "polyeq.sml: diff.behav. 5 in is_expended_in";
|
walther@59627
|
86 |
|
walther@60242
|
87 |
val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
|
walther@59627
|
88 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
|
walther@59868
|
89 |
if (UnparseC.term t) = "True" then ()
|
walther@59627
|
90 |
else error "polyeq.sml: diff.behav. in has_degree_in_in";
|
walther@59627
|
91 |
|
walther@60340
|
92 |
val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
|
walther@59627
|
93 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
|
walther@59868
|
94 |
if (UnparseC.term t) = "False" then ()
|
walther@59627
|
95 |
else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
|
walther@59627
|
96 |
|
walther@60340
|
97 |
val t4 = (Thm.term_of o the o (TermC.parse thy))
|
walther@60242
|
98 |
"((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
|
walther@59627
|
99 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
|
walther@59868
|
100 |
if (UnparseC.term t) = "False" then ()
|
walther@59627
|
101 |
else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
|
walther@59627
|
102 |
|
walther@60342
|
103 |
val t5 = (Thm.term_of o the o (TermC.parse thy))
|
walther@60242
|
104 |
"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
|
walther@59627
|
105 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
|
walther@59868
|
106 |
if (UnparseC.term t) = "True" then ()
|
walther@59627
|
107 |
else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
|
walther@59627
|
108 |
|
walther@59627
|
109 |
"----------- test matching problems --------------------------0---";
|
walther@59627
|
110 |
"----------- test matching problems --------------------------0---";
|
walther@59627
|
111 |
"----------- test matching problems --------------------------0---";
|
walther@60242
|
112 |
val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
113 |
if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
|
walther@59984
|
114 |
M_Match.Matches' {Find = [Correct "solutions L"],
|
walther@59627
|
115 |
With = [],
|
walther@60344
|
116 |
Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
|
walther@60344
|
117 |
Where = [Correct "matches (?a = 0) (- 8 - 2 * x + x \<up> 2 = 0)",
|
walther@60344
|
118 |
Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"],
|
walther@59627
|
119 |
Relate = []}
|
walther@59984
|
120 |
then () else error "M_Match.match_pbl [expanded,univariate,equation]";
|
walther@59627
|
121 |
|
walther@59997
|
122 |
if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
|
walther@59984
|
123 |
M_Match.Matches' {Find = [Correct "solutions L"],
|
walther@59627
|
124 |
With = [],
|
walther@60344
|
125 |
Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
|
walther@60344
|
126 |
Where = [Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"],
|
walther@59627
|
127 |
Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
|
walther@59984
|
128 |
then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]";
|
walther@59627
|
129 |
|
walther@59847
|
130 |
|
walther@59847
|
131 |
"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
|
walther@59847
|
132 |
"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
|
walther@59847
|
133 |
"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
|
walther@59847
|
134 |
(*##################################################################################
|
walther@60329
|
135 |
----------- 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
|
walther@59847
|
136 |
|
walther@59847
|
137 |
(*Aufgabe zum Einstieg in die Arbeit...*)
|
walther@60340
|
138 |
val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 2 = 0";
|
walther@59847
|
139 |
(*ein 'ruleset' aus Poly.ML wird angewandt...*)
|
walther@59847
|
140 |
val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
|
walther@59868
|
141 |
UnparseC.term t;
|
walther@60329
|
142 |
"a * b + (- 1 * (a * x) + (- 1 * (b * x) + x \<up> 2)) = 0";
|
walther@59847
|
143 |
val SOME (t,_) =
|
walther@59997
|
144 |
rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
|
walther@59868
|
145 |
UnparseC.term t;
|
walther@60329
|
146 |
"x \<up> 2 + (- 1 * (b * x) + (- 1 * (x * a) + b * a)) = 0";
|
walther@59847
|
147 |
(* bei Verwendung von "size_of-term" nach MG :*)
|
walther@60329
|
148 |
(*"x \<up> 2 + (- 1 * (b * x) + (b * a + - 1 * (x * a))) = 0" !!! *)
|
walther@59847
|
149 |
|
walther@59847
|
150 |
(*wir holen 'a' wieder aus der Klammerung heraus...*)
|
walther@59847
|
151 |
val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
|
walther@59868
|
152 |
UnparseC.term t;
|
walther@60329
|
153 |
"x \<up> 2 + - 1 * b * x + - 1 * x * a + b * a = 0";
|
walther@60329
|
154 |
(* "x \<up> 2 + - 1 * b * x + b * a + - 1 * x * a = 0" !!! *)
|
walther@59847
|
155 |
|
walther@59847
|
156 |
val SOME (t,_) =
|
walther@59997
|
157 |
rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
|
walther@59868
|
158 |
UnparseC.term t;
|
walther@60329
|
159 |
"x \<up> 2 + (- 1 * (b * x) + a * (b + - 1 * x)) = 0";
|
walther@59847
|
160 |
(*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
|
walther@60329
|
161 |
"x \<up> 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*)
|
walther@59847
|
162 |
|
walther@59847
|
163 |
(*das rewriting l"asst sich beobachten mit
|
walther@60330
|
164 |
Rewrite.trace_on := false; (*true false*)
|
walther@59847
|
165 |
*)
|
walther@59847
|
166 |
|
walther@60329
|
167 |
"------ 15.11.02 --------------------------";
|
walther@60340
|
168 |
val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";
|
walther@60340
|
169 |
val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
|
walther@60340
|
170 |
val a = (Thm.term_of o the o (TermC.parse thy)) "a";
|
walther@59847
|
171 |
|
walther@60330
|
172 |
Rewrite.trace_on := false; (*true false*)
|
walther@59847
|
173 |
(* Anwenden einer Regelmenge aus Termorder.ML: *)
|
walther@59847
|
174 |
val SOME (t,_) =
|
walther@59847
|
175 |
rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
|
walther@59868
|
176 |
UnparseC.term t;
|
walther@59847
|
177 |
val SOME (t,_) =
|
walther@59847
|
178 |
rewrite_set_ thy false discard_parentheses t;
|
walther@59868
|
179 |
UnparseC.term t;
|
walther@59847
|
180 |
"1 + b * x + x * a";
|
walther@59847
|
181 |
|
walther@60340
|
182 |
val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \<up> 2";
|
walther@59847
|
183 |
val SOME (t,_) =
|
walther@59847
|
184 |
rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
|
walther@59868
|
185 |
UnparseC.term t;
|
walther@59847
|
186 |
val SOME (t,_) =
|
walther@59847
|
187 |
rewrite_set_ thy false discard_parentheses t;
|
walther@59868
|
188 |
UnparseC.term t;
|
walther@60242
|
189 |
"1 + (x + b * x) * a + a \<up> 2";
|
walther@59847
|
190 |
|
walther@60340
|
191 |
val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
|
walther@59847
|
192 |
val SOME (t,_) =
|
walther@59847
|
193 |
rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
|
walther@59868
|
194 |
UnparseC.term t;
|
walther@59847
|
195 |
val SOME (t,_) =
|
walther@59847
|
196 |
rewrite_set_ thy false discard_parentheses t;
|
walther@59868
|
197 |
UnparseC.term t;
|
walther@60242
|
198 |
"1 + b * a + (7 + x) * a \<up> 2";
|
walther@59847
|
199 |
|
walther@59847
|
200 |
(* MG2003
|
walther@59847
|
201 |
Prog_Expr.thy grundlegende Algebra
|
walther@59847
|
202 |
Poly.thy Polynome
|
walther@59847
|
203 |
Rational.thy Br"uche
|
walther@59847
|
204 |
Root.thy Wurzeln
|
walther@59847
|
205 |
RootRat.thy Wurzen + Br"uche
|
walther@59847
|
206 |
Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
|
walther@59847
|
207 |
|
walther@59847
|
208 |
get_thm Termorder.thy "bdv_n_collect";
|
walther@59847
|
209 |
get_thm (theory "Isac_Knowledge") "bdv_n_collect";
|
walther@59847
|
210 |
*)
|
walther@60340
|
211 |
val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * x + 7 * a \<up> 2";
|
walther@59847
|
212 |
val SOME (t,_) =
|
walther@59847
|
213 |
rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
|
walther@59868
|
214 |
UnparseC.term t;
|
walther@59847
|
215 |
val SOME (t,_) =
|
walther@59847
|
216 |
rewrite_set_ thy false discard_parentheses t;
|
walther@59868
|
217 |
UnparseC.term t;
|
walther@60242
|
218 |
"(7 + x) * a \<up> 2";
|
walther@59847
|
219 |
|
walther@60230
|
220 |
val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi";
|
walther@59847
|
221 |
|
walther@59847
|
222 |
val t = (Thm.term_of o the o (parseold thy)) "7";
|
walther@59847
|
223 |
##################################################################################*)
|
walther@59847
|
224 |
|
walther@59847
|
225 |
|
walther@60342
|
226 |
"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
|
walther@60342
|
227 |
"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
|
walther@60342
|
228 |
"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
|
walther@60342
|
229 |
(* termorder hacked by MG, adapted later by WN *)
|
walther@60342
|
230 |
(** )local ( *. for make_polynomial_in .*)
|
walther@60342
|
231 |
|
walther@60342
|
232 |
open Term; (* for type order = EQUAL | LESS | GREATER *)
|
walther@60342
|
233 |
|
walther@60342
|
234 |
fun pr_ord EQUAL = "EQUAL"
|
walther@60342
|
235 |
| pr_ord LESS = "LESS"
|
walther@60342
|
236 |
| pr_ord GREATER = "GREATER";
|
walther@60342
|
237 |
|
walther@60342
|
238 |
fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0)
|
walther@60342
|
239 |
| dest_hd' x (t as Free (a, T)) =
|
walther@60342
|
240 |
if x = t then ((("|||||||||||||", 0), T), 0) (*WN*)
|
walther@60342
|
241 |
else (((a, 0), T), 1)
|
walther@60342
|
242 |
| dest_hd' _ (Var v) = (v, 2)
|
walther@60342
|
243 |
| dest_hd' _ (Bound i) = ((("", i), dummyT), 3)
|
walther@60342
|
244 |
| dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
|
walther@60342
|
245 |
| dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
|
walther@60342
|
246 |
|
walther@60342
|
247 |
fun size_of_term' i pr x (t as Const (\<^const_name>\<open>powr\<close>, _) $
|
walther@60342
|
248 |
Free (var, _) $ Free (pot, _)) =
|
walther@60342
|
249 |
(if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else ();
|
walther@60342
|
250 |
case x of (*WN*)
|
walther@60342
|
251 |
(Free (xstr, _)) =>
|
walther@60342
|
252 |
if xstr = var
|
walther@60342
|
253 |
then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else ();
|
walther@60342
|
254 |
1000 * (the (TermC.int_opt_of_string pot)))
|
walther@60342
|
255 |
else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "3") else (); 3)
|
walther@60342
|
256 |
| _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
|
walther@60342
|
257 |
| size_of_term' i pr x (t as Abs (_, _, body)) =
|
walther@60342
|
258 |
(if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else ();
|
walther@60342
|
259 |
1 + size_of_term' (i + 1) pr x body)
|
walther@60342
|
260 |
| size_of_term' i pr x (f $ t) =
|
walther@60342
|
261 |
let
|
walther@60342
|
262 |
val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else ();
|
walther@60342
|
263 |
val s1 = size_of_term' (i + 1) pr x f
|
walther@60342
|
264 |
val s2 = size_of_term' (i + 1) pr x t
|
walther@60342
|
265 |
val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$-->: " ^ string_of_int s1 ^ " + " ^ string_of_int s2 ^ " = " ^ string_of_int(s1 + s2)) else ();
|
walther@60342
|
266 |
in (s1 + s2) end
|
walther@60342
|
267 |
| size_of_term' i pr x t =
|
walther@60342
|
268 |
(if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else ();
|
walther@60342
|
269 |
case t of
|
walther@60342
|
270 |
Free (subst, _) =>
|
walther@60342
|
271 |
(case x of
|
walther@60342
|
272 |
Free (xstr, _) =>
|
walther@60342
|
273 |
if xstr = subst
|
walther@60342
|
274 |
then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000)
|
walther@60342
|
275 |
else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "1") else (); 1)
|
walther@60342
|
276 |
| _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
|
walther@60342
|
277 |
| _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1));
|
walther@60342
|
278 |
|
walther@60342
|
279 |
fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
|
walther@60342
|
280 |
let
|
walther@60342
|
281 |
val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else ();
|
walther@60342
|
282 |
val ord =
|
walther@60342
|
283 |
case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord
|
walther@60342
|
284 |
val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else ()
|
walther@60342
|
285 |
in ord end
|
walther@60342
|
286 |
| term_ord' i pr x _ (t, u) =
|
walther@60342
|
287 |
let
|
walther@60342
|
288 |
val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else ();
|
walther@60342
|
289 |
val ord =
|
walther@60342
|
290 |
case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of
|
walther@60342
|
291 |
EQUAL =>
|
walther@60342
|
292 |
let val (f, ts) = strip_comb t and (g, us) = strip_comb u
|
walther@60342
|
293 |
in
|
walther@60342
|
294 |
(case hd_ord (i + 1) pr x (f, g) of
|
walther@60342
|
295 |
EQUAL => (terms_ord x (i + 1) pr) (ts, us)
|
walther@60342
|
296 |
| ord => ord)
|
walther@60342
|
297 |
end
|
walther@60342
|
298 |
| ord => ord
|
walther@60342
|
299 |
val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else ()
|
walther@60342
|
300 |
in ord end
|
walther@60342
|
301 |
and hd_ord i pr x (f, g) = (* ~ term.ML *)
|
walther@60342
|
302 |
let
|
walther@60342
|
303 |
val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else ();
|
walther@60342
|
304 |
val ord = prod_ord
|
walther@60342
|
305 |
(prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
|
walther@60342
|
306 |
(dest_hd' x f, dest_hd' x g)
|
walther@60342
|
307 |
val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else ();
|
walther@60342
|
308 |
in ord end
|
walther@60342
|
309 |
and terms_ord x i pr (ts, us) =
|
walther@60342
|
310 |
let
|
walther@60342
|
311 |
val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else ();
|
walther@60342
|
312 |
val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us);
|
walther@60342
|
313 |
val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else ();
|
walther@60342
|
314 |
in ord end
|
walther@60342
|
315 |
|
walther@60342
|
316 |
(** )in( *local*)
|
walther@60342
|
317 |
|
walther@60342
|
318 |
fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) =
|
walther@60342
|
319 |
((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **)
|
walther@60342
|
320 |
case subst of
|
walther@60342
|
321 |
(_, x) :: _ =>
|
walther@60342
|
322 |
term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS
|
walther@60342
|
323 |
| _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst))
|
walther@60342
|
324 |
|
walther@60342
|
325 |
(** )end;( *local*)
|
walther@60342
|
326 |
|
walther@60342
|
327 |
val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
|
walther@60393
|
328 |
if ord_make_polynomial_in false(*true*) @{theory} subs (t1, t2) then () else error "still GREATER?";
|
walther@60342
|
329 |
|
walther@60342
|
330 |
val x = TermC.str2term "x ::real";
|
walther@60342
|
331 |
|
walther@60342
|
332 |
val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \<up> 2 / 4 ::real");
|
walther@60393
|
333 |
if 2006 = size_of_term' 1 false(*true*) x t1
|
walther@60342
|
334 |
then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)";
|
walther@60342
|
335 |
|
walther@60342
|
336 |
val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \<up> 3) :: real");
|
walther@60393
|
337 |
if 3004 = size_of_term' 1 false(*true*) x t2
|
walther@60342
|
338 |
then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED";
|
walther@60342
|
339 |
|
walther@60342
|
340 |
|
walther@59847
|
341 |
"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
|
walther@59847
|
342 |
"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
|
walther@59847
|
343 |
"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
|
walther@60340
|
344 |
val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")];
|
walther@60340
|
345 |
val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];
|
walther@60340
|
346 |
val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")];
|
walther@59847
|
347 |
|
walther@60340
|
348 |
val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x";
|
walther@60340
|
349 |
val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
|
walther@60340
|
350 |
val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
|
walther@60340
|
351 |
val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
|
walther@59847
|
352 |
|
walther@60393
|
353 |
if ord_make_polynomial_in false(*true*) thy substx (x1,x2) = true(*LESS *) then ()
|
walther@59847
|
354 |
else error "termorder.sml diff.behav ord_make_polynomial_in #1";
|
walther@59847
|
355 |
|
walther@60393
|
356 |
if ord_make_polynomial_in false(*true*) thy substa (x1,x2) = true(*LESS *) then ()
|
walther@59847
|
357 |
else error "termorder.sml diff.behav ord_make_polynomial_in #2";
|
walther@59847
|
358 |
|
walther@60393
|
359 |
if ord_make_polynomial_in false(*true*) thy substb (x1,x2) = false(*GREATER*) then ()
|
walther@59847
|
360 |
else error "termorder.sml diff.behav ord_make_polynomial_in #3";
|
walther@59847
|
361 |
|
walther@60340
|
362 |
val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
|
walther@60340
|
363 |
val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
|
walther@60393
|
364 |
ord_make_polynomial_in false(*true*) thy substx (aa, bb);
|
walther@59847
|
365 |
true; (* => LESS *)
|
walther@59847
|
366 |
|
walther@60340
|
367 |
val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
|
walther@60340
|
368 |
val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
|
walther@60393
|
369 |
ord_make_polynomial_in false(*true*) thy substa (aa, bb);
|
walther@59847
|
370 |
false; (* => GREATER *)
|
walther@59847
|
371 |
|
walther@59847
|
372 |
(* und nach dem Re-engineering der Termorders in den 'rulesets'
|
walther@59847
|
373 |
kannst Du die 'gr"osste' Variable frei w"ahlen: *)
|
walther@60344
|
374 |
val bdv= TermC.str2term "bdv ::real";
|
walther@60344
|
375 |
val x = TermC.str2term "x ::real";
|
walther@60344
|
376 |
val a = TermC.str2term "a ::real";
|
walther@60344
|
377 |
val b = TermC.str2term "b ::real";
|
walther@59847
|
378 |
val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
|
walther@59868
|
379 |
if UnparseC.term t' = "b + x + a" then ()
|
walther@59847
|
380 |
else error "termorder.sml diff.behav ord_make_polynomial_in #11";
|
walther@59847
|
381 |
|
walther@59847
|
382 |
val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
|
walther@59847
|
383 |
|
walther@59847
|
384 |
val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
|
walther@59868
|
385 |
if UnparseC.term t' = "a + b + x" then ()
|
walther@59847
|
386 |
else error "termorder.sml diff.behav ord_make_polynomial_in #13";
|
walther@59847
|
387 |
|
walther@60329
|
388 |
val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
|
walther@60340
|
389 |
val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
|
walther@59847
|
390 |
val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
|
walther@60344
|
391 |
if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2" then ()
|
walther@59847
|
392 |
else error "termorder.sml diff.behav ord_make_polynomial_in #15";
|
walther@59847
|
393 |
|
walther@60342
|
394 |
val ttt' = "(3*x + 5)/18 ::real";
|
walther@60340
|
395 |
val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
|
walther@59847
|
396 |
val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
|
walther@59868
|
397 |
if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
|
walther@59847
|
398 |
else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
|
walther@59847
|
399 |
|
walther@59847
|
400 |
val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
|
walther@59868
|
401 |
if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
|
walther@59847
|
402 |
else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
|
walther@59847
|
403 |
|
walther@59627
|
404 |
"----------- lin.eq degree_0 -------------------------------------";
|
walther@59627
|
405 |
"----------- lin.eq degree_0 -------------------------------------";
|
walther@59627
|
406 |
"----------- lin.eq degree_0 -------------------------------------";
|
walther@59627
|
407 |
"----- d0_false ------";
|
walther@59627
|
408 |
val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
|
walther@59997
|
409 |
val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
|
walther@59997
|
410 |
["PolyEq", "solve_d0_polyeq_equation"]);
|
walther@59871
|
411 |
(*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ========
|
walther@60329
|
412 |
TODO: change to "equality (x + - 1*x = (0::real))"
|
walther@59627
|
413 |
and search for an appropriate problem and method.
|
walther@59627
|
414 |
|
walther@59627
|
415 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
416 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
417 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
418 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
419 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
420 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
421 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59959
|
422 |
case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
|
walther@59627
|
423 |
| _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
|
walther@59627
|
424 |
|
walther@59627
|
425 |
"----- d0_true ------";
|
walther@59997
|
426 |
val fmz = ["equality (0 = (0::real))", "solveFor x", "solutions L"];
|
walther@59997
|
427 |
val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
|
walther@59997
|
428 |
["PolyEq", "solve_d0_polyeq_equation"]);
|
walther@59627
|
429 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
430 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
431 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
432 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
433 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
434 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
435 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59959
|
436 |
case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
|
walther@59627
|
437 |
| _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
|
walther@59627
|
438 |
============ inhibit exn WN110914 ============================================*)
|
walther@59627
|
439 |
|
walther@59627
|
440 |
"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
|
walther@59627
|
441 |
"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
|
walther@59627
|
442 |
"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
|
walther@59627
|
443 |
"----- d2_pqformula1 ------!!!!";
|
walther@60329
|
444 |
val fmz = ["equality (- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real))", "solveFor z", "solutions L"];
|
walther@59627
|
445 |
val (dI',pI',mI') =
|
walther@59997
|
446 |
("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]);
|
walther@59627
|
447 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
448 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
449 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
450 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
451 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
452 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
453 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
454 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
|
walther@59627
|
455 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
456 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
457 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
458 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
459 |
|
walther@60329
|
460 |
(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2] TODO sqrt*)
|
walther@59627
|
461 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
|
walther@59921
|
462 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59921
|
463 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59921
|
464 |
|
walther@59921
|
465 |
if p = ([], Res) andalso
|
walther@60329
|
466 |
f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2]" then
|
walther@60329
|
467 |
case nxt of End_Proof' => () | _ => error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 1"
|
walther@60329
|
468 |
else error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 2";
|
walther@59627
|
469 |
|
walther@60329
|
470 |
"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
|
walther@60329
|
471 |
"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
|
walther@60329
|
472 |
"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
|
walther@59627
|
473 |
"----- d2_pqformula1_neg ------";
|
walther@60329
|
474 |
val fmz = ["equality (2 +(- 1)*x + x \<up> 2 = (0::real))", "solveFor x", "solutions L"];
|
walther@59997
|
475 |
val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
476 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
477 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
478 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
479 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
480 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
481 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
482 |
(*### or2list False
|
walther@59627
|
483 |
([1],Res) False Or_to_List)*)
|
walther@59627
|
484 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
485 |
(*### or2list False
|
walther@59627
|
486 |
([2],Res) [] Check_elementwise "Assumptions"*)
|
walther@59627
|
487 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
488 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59844
|
489 |
val asm = Ctree.get_assumptions pt p;
|
walther@59627
|
490 |
if f2str f = "[]" andalso
|
walther@60329
|
491 |
UnparseC.terms asm = "[\"lhs (2 + - 1 * x + x \<up> 2 = 0) is_poly_in x\", " ^
|
walther@60329
|
492 |
"\"lhs (2 + - 1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then ()
|
walther@60329
|
493 |
else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \<up> 2 = 0";
|
walther@59627
|
494 |
|
walther@60329
|
495 |
"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
|
walther@60329
|
496 |
"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
|
walther@60329
|
497 |
"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
|
walther@59627
|
498 |
"----- d2_pqformula2 ------";
|
walther@60329
|
499 |
val fmz = ["equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
500 |
val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
501 |
["PolyEq", "solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
502 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
503 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
504 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
505 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
506 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
507 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
508 |
|
walther@59627
|
509 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
510 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
511 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
512 |
case f of Test_Out.FormKF "[x = 2, x = - 1]" => ()
|
walther@60329
|
513 |
| _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]";
|
walther@59627
|
514 |
|
walther@59627
|
515 |
|
walther@60329
|
516 |
"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
|
walther@60329
|
517 |
"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
|
walther@60329
|
518 |
"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
|
walther@59627
|
519 |
"----- d2_pqformula3 ------";
|
walther@59627
|
520 |
(*EP-9*)
|
walther@60329
|
521 |
val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
522 |
val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
523 |
["PolyEq", "solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
524 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
525 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
526 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
527 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
528 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
529 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
530 |
|
walther@59627
|
531 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
532 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
533 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
534 |
case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
|
walther@60329
|
535 |
| _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0-> [x = 1, x = - 2]";
|
walther@59627
|
536 |
|
walther@59627
|
537 |
|
walther@60242
|
538 |
"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
|
walther@60242
|
539 |
"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
|
walther@60242
|
540 |
"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
|
walther@59627
|
541 |
"----- d2_pqformula3_neg ------";
|
walther@60242
|
542 |
val fmz = ["equality (2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
543 |
val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
544 |
["PolyEq", "solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
545 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
546 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
547 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
548 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
549 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
550 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
551 |
|
walther@59627
|
552 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
553 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60242
|
554 |
"TODO 2 + x + x \<up> 2 = 0";
|
walther@60242
|
555 |
"TODO 2 + x + x \<up> 2 = 0";
|
walther@60242
|
556 |
"TODO 2 + x + x \<up> 2 = 0";
|
walther@59627
|
557 |
|
walther@60329
|
558 |
"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
|
walther@60329
|
559 |
"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
|
walther@60329
|
560 |
"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
|
walther@59627
|
561 |
"----- d2_pqformula4 ------";
|
walther@60329
|
562 |
val fmz = ["equality (- 2 + x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
563 |
val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
564 |
["PolyEq", "solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
565 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
566 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
567 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
568 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
569 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
570 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
571 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
572 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
573 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
574 |
case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
|
walther@60329
|
575 |
| _ => error "polyeq.sml: diff.behav. in - 2 + x + 1*x \<up> 2 = 0 -> [x = 1, x = - 2]";
|
walther@59627
|
576 |
|
walther@60242
|
577 |
"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
|
walther@60242
|
578 |
"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
|
walther@60242
|
579 |
"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
|
walther@59627
|
580 |
"----- d2_pqformula5 ------";
|
walther@60242
|
581 |
val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
582 |
val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
583 |
["PolyEq", "solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
584 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
585 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
586 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
587 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
588 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
589 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
590 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
591 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
592 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
593 |
case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
|
walther@60329
|
594 |
| _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = - 1]";
|
walther@59627
|
595 |
|
walther@60242
|
596 |
"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
|
walther@60242
|
597 |
"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
|
walther@60242
|
598 |
"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
|
walther@59627
|
599 |
"----- d2_pqformula6 ------";
|
walther@60242
|
600 |
val fmz = ["equality (1*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
601 |
val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
602 |
["PolyEq", "solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
603 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
604 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
605 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
606 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
607 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
608 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
609 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
610 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
611 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
612 |
case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
|
walther@60329
|
613 |
| _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = - 1]";
|
walther@59627
|
614 |
|
walther@60242
|
615 |
"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
|
walther@60242
|
616 |
"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
|
walther@60242
|
617 |
"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
|
walther@59627
|
618 |
"----- d2_pqformula7 ------";
|
walther@60329
|
619 |
(*EP- 10*)
|
walther@60242
|
620 |
val fmz = ["equality ( x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
621 |
val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
622 |
["PolyEq", "solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
623 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
624 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
625 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
626 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
627 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
628 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
629 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
630 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
631 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
632 |
case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
|
walther@60329
|
633 |
| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
|
walther@59627
|
634 |
|
walther@60242
|
635 |
"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
|
walther@60242
|
636 |
"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
|
walther@60242
|
637 |
"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
|
walther@59627
|
638 |
"----- d2_pqformula8 ------";
|
walther@60242
|
639 |
val fmz = ["equality (x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
640 |
val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
641 |
["PolyEq", "solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
642 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
643 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
644 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
645 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
646 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
647 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
648 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
649 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
650 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
651 |
case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
|
walther@60329
|
652 |
| _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = - 1]";
|
walther@59627
|
653 |
|
walther@60242
|
654 |
"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
|
walther@60242
|
655 |
"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
|
walther@60242
|
656 |
"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
|
walther@59627
|
657 |
"----- d2_pqformula9 ------";
|
walther@60242
|
658 |
val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
659 |
val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
660 |
["PolyEq", "solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
661 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
662 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
663 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
664 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
665 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
666 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
667 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
668 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
669 |
case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
|
walther@60329
|
670 |
| _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
|
walther@59627
|
671 |
|
walther@59627
|
672 |
|
walther@60242
|
673 |
"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
|
walther@60242
|
674 |
"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
|
walther@60242
|
675 |
"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
|
walther@59627
|
676 |
"----- d2_pqformula9_neg ------";
|
walther@60242
|
677 |
val fmz = ["equality (4 + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
678 |
val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
679 |
["PolyEq", "solve_d2_polyeq_pq_equation"]);
|
walther@59627
|
680 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
681 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
682 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
683 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
684 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
685 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
686 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60242
|
687 |
"TODO 4 + 1*x \<up> 2 = 0";
|
walther@60242
|
688 |
"TODO 4 + 1*x \<up> 2 = 0";
|
walther@60242
|
689 |
"TODO 4 + 1*x \<up> 2 = 0";
|
walther@59627
|
690 |
|
walther@59627
|
691 |
"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
|
walther@59627
|
692 |
"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
|
walther@59627
|
693 |
"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
|
walther@60329
|
694 |
val fmz = ["equality (- 1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
695 |
val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
696 |
["PolyEq", "solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
697 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
698 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
699 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
700 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
701 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
702 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
703 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
704 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
705 |
case f of Test_Out.FormKF "[x = 1, x = - 1 / 2]" => ()
|
walther@60329
|
706 |
| _ => error "polyeq.sml: diff.behav. in - 1 + (- 1)*x + 2*x^2 = 0 -> [x = 1, x = - 1/2]";
|
walther@59627
|
707 |
|
walther@60329
|
708 |
"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
|
walther@60329
|
709 |
"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
|
walther@60329
|
710 |
"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
|
walther@60329
|
711 |
val fmz = ["equality (1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
712 |
val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
713 |
["PolyEq", "solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
714 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
715 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
716 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
717 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
718 |
|
walther@59627
|
719 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
720 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
721 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
722 |
"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
|
walther@60329
|
723 |
"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
|
walther@60329
|
724 |
"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
|
walther@59627
|
725 |
|
walther@59627
|
726 |
|
walther@60329
|
727 |
"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
|
walther@60329
|
728 |
"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
|
walther@60329
|
729 |
"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
|
walther@60329
|
730 |
(*EP- 11*)
|
walther@60329
|
731 |
val fmz = ["equality (- 1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
732 |
val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
733 |
["PolyEq", "solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
734 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
735 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
736 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
737 |
|
walther@59627
|
738 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
739 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
740 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
741 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
742 |
|
walther@59627
|
743 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
744 |
case f of Test_Out.FormKF "[x = 1 / 2, x = - 1]" => ()
|
walther@60329
|
745 |
| _ => error "polyeq.sml: diff.behav. in - 1 + x + 2*x^2 = 0 -> [x = 1/2, x = - 1]";
|
walther@59627
|
746 |
|
walther@59627
|
747 |
|
walther@60242
|
748 |
"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
|
walther@60242
|
749 |
"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
|
walther@60242
|
750 |
"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
|
walther@60242
|
751 |
val fmz = ["equality (1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
752 |
val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
753 |
["PolyEq", "solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
754 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
755 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
756 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
757 |
|
walther@59627
|
758 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
759 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
760 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
761 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
762 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60242
|
763 |
"TODO 1 + x + 2*x \<up> 2 = 0";
|
walther@60242
|
764 |
"TODO 1 + x + 2*x \<up> 2 = 0";
|
walther@60242
|
765 |
"TODO 1 + x + 2*x \<up> 2 = 0";
|
walther@59627
|
766 |
|
walther@59627
|
767 |
|
walther@60329
|
768 |
val fmz = ["equality (- 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
769 |
val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
770 |
["PolyEq", "solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
771 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
772 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
773 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
774 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
775 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
776 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
777 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
778 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
779 |
case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
|
walther@60329
|
780 |
| _ => error "polyeq.sml: diff.behav. in - 2 + 1*x + x^2 = 0 -> [x = 1, x = - 2]";
|
walther@59627
|
781 |
|
walther@60242
|
782 |
val fmz = ["equality ( 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
783 |
val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
784 |
["PolyEq", "solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
785 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
786 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
787 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
788 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
789 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
790 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
791 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
792 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60242
|
793 |
"TODO 2 + 1*x + x \<up> 2 = 0";
|
walther@60242
|
794 |
"TODO 2 + 1*x + x \<up> 2 = 0";
|
walther@60242
|
795 |
"TODO 2 + 1*x + x \<up> 2 = 0";
|
walther@59627
|
796 |
|
walther@60329
|
797 |
(*EP- 12*)
|
walther@60329
|
798 |
val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
799 |
val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
800 |
["PolyEq", "solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
801 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
802 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
803 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
804 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
805 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
806 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
807 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
808 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
809 |
case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
|
walther@60329
|
810 |
| _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0 -> [x = 1, x = - 2]";
|
walther@59627
|
811 |
|
walther@60242
|
812 |
val fmz = ["equality ( 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
813 |
val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
814 |
["PolyEq", "solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
815 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
816 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
817 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
818 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
819 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
820 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
821 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
822 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60242
|
823 |
"TODO 2 + x + x \<up> 2 = 0";
|
walther@60242
|
824 |
"TODO 2 + x + x \<up> 2 = 0";
|
walther@60242
|
825 |
"TODO 2 + x + x \<up> 2 = 0";
|
walther@59627
|
826 |
|
walther@60329
|
827 |
(*EP- 13*)
|
walther@60242
|
828 |
val fmz = ["equality (-8 + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
829 |
val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
830 |
["PolyEq", "solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
831 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
832 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
833 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
834 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
835 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
836 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
837 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
838 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
839 |
case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
|
walther@60329
|
840 |
| _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = - 2]";
|
walther@59627
|
841 |
|
walther@60242
|
842 |
val fmz = ["equality ( 8+ 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
843 |
val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
844 |
["PolyEq", "solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
845 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
846 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
847 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
848 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
849 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
850 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
851 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60242
|
852 |
"TODO 8+ 2*x \<up> 2 = 0";
|
walther@60242
|
853 |
"TODO 8+ 2*x \<up> 2 = 0";
|
walther@60242
|
854 |
"TODO 8+ 2*x \<up> 2 = 0";
|
walther@59627
|
855 |
|
walther@60329
|
856 |
(*EP- 14*)
|
walther@60242
|
857 |
val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
858 |
val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
859 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
860 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
861 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
862 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
863 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
864 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
865 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
866 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
867 |
case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
|
walther@60329
|
868 |
| _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
|
walther@59627
|
869 |
|
walther@59627
|
870 |
|
walther@60242
|
871 |
val fmz = ["equality ( 4+ x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
872 |
val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
873 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
874 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
875 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
876 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
877 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
878 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
879 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60242
|
880 |
"TODO 4+ x \<up> 2 = 0";
|
walther@60242
|
881 |
"TODO 4+ x \<up> 2 = 0";
|
walther@60242
|
882 |
"TODO 4+ x \<up> 2 = 0";
|
walther@59627
|
883 |
|
walther@60329
|
884 |
(*EP- 15*)
|
walther@60242
|
885 |
val fmz = ["equality (2*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
886 |
val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
887 |
["PolyEq", "solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
888 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
889 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
890 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
891 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
892 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
893 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
894 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
895 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
896 |
case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
|
walther@60329
|
897 |
| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
|
walther@59627
|
898 |
|
walther@60242
|
899 |
val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
900 |
val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
901 |
["PolyEq", "solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
902 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
903 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
904 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
905 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
906 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
907 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
908 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
909 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
910 |
case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
|
walther@60329
|
911 |
| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
|
walther@59627
|
912 |
|
walther@60329
|
913 |
(*EP- 16*)
|
walther@60393
|
914 |
val fmz = ["equality (x + 2 * x \<up> 2 = (0::real))", "solveFor (x::real)", "solutions L"];
|
walther@59997
|
915 |
val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
916 |
["PolyEq", "solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
917 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
918 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
919 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
920 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
921 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60393
|
922 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60393
|
923 |
|
walther@60393
|
924 |
(*+*)val Test_Out.FormKF "x + 2 * x \<up> 2 = 0" = f;
|
walther@60393
|
925 |
(*+*)val Rewrite_Set_Inst (["(''bdv'', x)"], "d2_polyeq_abcFormula_simplify") = nxt
|
walther@60393
|
926 |
|
walther@60393
|
927 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*"x + 2 * x \<up> 2 = 0", d2_polyeq_abcFormula_simplify*)
|
walther@59627
|
928 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
929 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
930 |
case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => ()
|
walther@60329
|
931 |
| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1 / 2]";
|
walther@59627
|
932 |
|
walther@59627
|
933 |
(*EP-//*)
|
walther@60242
|
934 |
val fmz = ["equality (x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
|
walther@59997
|
935 |
val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
|
walther@59997
|
936 |
["PolyEq", "solve_d2_polyeq_abc_equation"]);
|
walther@59627
|
937 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
938 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
939 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
940 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
941 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
942 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
943 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
944 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
945 |
case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
|
walther@60329
|
946 |
| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
|
walther@59627
|
947 |
|
walther@59627
|
948 |
|
walther@60242
|
949 |
"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
|
walther@60242
|
950 |
"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
|
walther@60242
|
951 |
"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
|
walther@59627
|
952 |
(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
|
walther@59627
|
953 |
see --- val rls = calculate_RootRat > calculate_Rational ---
|
walther@59627
|
954 |
calculate_RootRat was a TODO with 2002, requires re-design.
|
walther@60242
|
955 |
see also --- (-8 - 2*x + x \<up> 2 = 0), by rewriting --- below
|
walther@59627
|
956 |
*)
|
walther@60242
|
957 |
val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
|
walther@59997
|
958 |
"solveFor x", "solutions L"];
|
walther@59627
|
959 |
val (dI',pI',mI') =
|
walther@59997
|
960 |
("PolyEq",["degree_2", "expanded", "univariate", "equation"],
|
walther@59997
|
961 |
["PolyEq", "complete_square"]);
|
walther@59627
|
962 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
963 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
964 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
965 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
966 |
|
walther@59627
|
967 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59997
|
968 |
(*Apply_Method ("PolyEq", "complete_square")*)
|
walther@59627
|
969 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60242
|
970 |
(*"-8 - 2 * x + x \<up> 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
|
walther@59627
|
971 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60242
|
972 |
(*"-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2", nxt = Rewrite("square_explicit1"*)
|
walther@59627
|
973 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60242
|
974 |
(*"(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8" nxt = Rewrite("root_plus_minus*)
|
walther@59627
|
975 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60242
|
976 |
(*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
|
walther@60242
|
977 |
2 / 2 - x = - sqrt ((2 / 2) \<up> 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
|
walther@59627
|
978 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60242
|
979 |
(*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
|
walther@60329
|
980 |
- 1*x = - (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8)"nxt = R_Inst("bdv_explt2"*)
|
walther@59627
|
981 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
982 |
(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
|
walther@60329
|
983 |
- 1 * x = (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = bdv_explicit3*)
|
walther@59627
|
984 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
985 |
(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
|
walther@60329
|
986 |
x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))" nxt = bdv_explicit3*)
|
walther@59627
|
987 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
988 |
(*"x = - 1 * (- (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8)) |
|
walther@60329
|
989 |
x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = calculate_Rational
|
walther@60242
|
990 |
NOT IMPLEMENTED SINCE 2002 ------------------------------ \<up> \<up> \<up> \<up> \<up> \<up> *)
|
walther@59627
|
991 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
992 |
(*"x = - 2 | x = 4" nxt = Or_to_List*)
|
walther@59627
|
993 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60329
|
994 |
(*"[x = - 2, x = 4]" nxt = Check_Postcond*)
|
walther@59627
|
995 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
|
walther@59627
|
996 |
(* FIXXXME
|
walther@60329
|
997 |
case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2, x = 4]")) => () TODO
|
walther@60329
|
998 |
| _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]";
|
walther@59627
|
999 |
*)
|
walther@59627
|
1000 |
if f2str f =
|
walther@60393
|
1001 |
"[x = - 1 * - 1 + - 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8))]"
|
walther@60329
|
1002 |
(*"[x = - 1 * - 1 + - 1 * sqrt (1 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \<up> 2 - -8))]"*)
|
walther@60329
|
1003 |
then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]";
|
walther@59627
|
1004 |
|
walther@59627
|
1005 |
|
walther@60242
|
1006 |
"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
|
walther@60242
|
1007 |
"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
|
walther@60242
|
1008 |
"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
|
walther@60393
|
1009 |
(*stopped due to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
|
walther@59627
|
1010 |
see --- val rls = calculate_RootRat > calculate_Rational ---*)
|
walther@59627
|
1011 |
val thy = @{theory PolyEq};
|
walther@59627
|
1012 |
val ctxt = Proof_Context.init_global thy;
|
walther@59627
|
1013 |
val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
|
walther@60242
|
1014 |
val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)";
|
walther@59627
|
1015 |
|
walther@59627
|
1016 |
val rls = complete_square;
|
walther@59627
|
1017 |
val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
|
walther@60393
|
1018 |
if UnparseC.term t = "- 8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2"
|
walther@60393
|
1019 |
then () else error "rls complete_square CHANGED";
|
walther@59627
|
1020 |
|
walther@60393
|
1021 |
val thm = @{thm square_explicit1};
|
walther@59851
|
1022 |
val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
|
walther@60393
|
1023 |
if UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - - 8"
|
walther@60393
|
1024 |
then () else error "thm square_explicit1 CHANGED";
|
walther@59627
|
1025 |
|
walther@60393
|
1026 |
val thm = @{thm root_plus_minus};
|
walther@59627
|
1027 |
val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
|
walther@60393
|
1028 |
if UnparseC.term t =
|
walther@60393
|
1029 |
"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
|
walther@60393
|
1030 |
then () else error "thm root_plus_minus CHANGED";
|
walther@59627
|
1031 |
|
walther@59627
|
1032 |
(*the thm bdv_explicit2* here required to be constrained to ::real*)
|
walther@60393
|
1033 |
val thm = @{thm bdv_explicit2};
|
walther@59851
|
1034 |
val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
|
walther@60393
|
1035 |
if UnparseC.term t =
|
walther@60393
|
1036 |
"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
|
walther@60393
|
1037 |
then () else error "thm bdv_explicit2 CHANGED";
|
walther@59627
|
1038 |
|
walther@60393
|
1039 |
val thm = @{thm bdv_explicit3};
|
walther@59851
|
1040 |
val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
|
walther@60393
|
1041 |
if UnparseC.term t =
|
walther@60393
|
1042 |
"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
|
walther@60393
|
1043 |
then () else error "thm bdv_explicit3 CHANGED";
|
walther@59627
|
1044 |
|
walther@60393
|
1045 |
val thm = @{thm bdv_explicit2};
|
walther@59851
|
1046 |
val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
|
walther@60393
|
1047 |
if UnparseC.term t =
|
walther@60393
|
1048 |
"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
|
walther@60393
|
1049 |
then () else error "thm bdv_explicit2 CHANGED";
|
walther@59627
|
1050 |
|
walther@59627
|
1051 |
val rls = calculate_RootRat;
|
walther@59627
|
1052 |
val SOME (t,asm) = rewrite_set_ thy true rls t;
|
walther@59868
|
1053 |
if UnparseC.term t =
|
walther@60393
|
1054 |
"- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - - 8) \<or>\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8))"
|
walther@60329
|
1055 |
(*"- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - -8) |\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8))"..isabisac15*)
|
walther@60242
|
1056 |
then () else error "(-8 - 2*x + x \<up> 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
|
walther@60329
|
1057 |
(*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*)
|
walther@59627
|
1058 |
|
walther@59627
|
1059 |
|
walther@60242
|
1060 |
"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
|
walther@60242
|
1061 |
"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
|
walther@60242
|
1062 |
"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
|
walther@59627
|
1063 |
"---- test the erls ----";
|
walther@60340
|
1064 |
val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1";
|
walther@59627
|
1065 |
val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
|
walther@59868
|
1066 |
val t' = UnparseC.term t;
|
wenzelm@60309
|
1067 |
(*if t'= \<^const_name>\<open>True\<close> then ()
|
walther@59627
|
1068 |
else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
|
walther@59627
|
1069 |
(* *)
|
walther@60242
|
1070 |
val fmz = ["equality (3 - 10*x + 3*x \<up> 2 = 0)",
|
walther@59997
|
1071 |
"solveFor x", "solutions L"];
|
walther@59627
|
1072 |
val (dI',pI',mI') =
|
walther@59997
|
1073 |
("PolyEq",["degree_2", "expanded", "univariate", "equation"],
|
walther@59997
|
1074 |
["PolyEq", "complete_square"]);
|
walther@59627
|
1075 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
1076 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1077 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1078 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1079 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1080 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1081 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1082 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59997
|
1083 |
(*Apply_Method ("PolyEq", "complete_square")*)
|
walther@59627
|
1084 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
|
walther@59627
|
1085 |
|
walther@60329
|
1086 |
"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
|
walther@60329
|
1087 |
"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
|
walther@60329
|
1088 |
"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
|
walther@60329
|
1089 |
val fmz = ["equality (- 16 + 4*x + 2*x \<up> 2 = 0)",
|
walther@59997
|
1090 |
"solveFor x", "solutions L"];
|
walther@59627
|
1091 |
val (dI',pI',mI') =
|
walther@59997
|
1092 |
("PolyEq",["degree_2", "expanded", "univariate", "equation"],
|
walther@59997
|
1093 |
["PolyEq", "complete_square"]);
|
walther@59627
|
1094 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59627
|
1095 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1096 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1097 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1098 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1099 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1100 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1101 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59997
|
1102 |
(*Apply_Method ("PolyEq", "complete_square")*)
|
walther@59627
|
1103 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1104 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1105 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1106 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1107 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1108 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1109 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1110 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1111 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1112 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59627
|
1113 |
(* FIXXXXME n1.,
|
walther@59959
|
1114 |
case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
|
walther@59627
|
1115 |
| _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
|
walther@59627
|
1116 |
*)
|
walther@59627
|
1117 |
|