1 (* use"../smltest/IsacKnowledge/rlang.sml";
5 (******************************************************************
6 WN.060104 transfer marked (*E..*)examples to the exp-collection
7 # exp_IsacCore_Equ_Uni_Poly.xml from rlang.sml (*EP*) exp
8 # exp_IsacCore_Equ_Uni_Rat.xml from rlang.sml (*ER*) exp
9 # exp_IsacCore_Equ_Uni_Root.xml from rlang.sml (*EO*) exp
10 *******************************************************************)
14 (*WN.12.6.03: for TODOs search 'writeln', for simplification search MG*)
15 (* use"kbtest/rlang.sml";
18 tests over all equations implemented in his diploma thesis
19 Elementare Gleichungen der Mittelschulmathematik in der ISAC Wissensbasis,
20 Master's thesis, University of Technology, Graz, Austria, March 2003.
26 author = {Schalk, Heinz-Christian and Binder, Christian and Fertl, Walter and
27 Firneis, Friedrich and Gems, Werner and Lehner, Dieter and
28 Plihal, Andreas and Würl,Manfred},
29 title = {Mathematik für höhere technische Lehranstalten Band I},
30 publisher = {Reniets Verlag},
32 note = {Schulbuch-Nr. 942},
36 author = {Schalk, Heinz-Christian and Baumgartner, Gerhard and Binder, Christian and
37 Eder, Hans Gerhard and Fertl, Walter and Firneis, Friedrich and
38 Konstantiniuk, Peter and Plihal, Andreas and Rümmele, Goswin and
39 Steinwender, Andreas and Zangerl, Nikolaus},
40 title = {Mathematik für höhere technische Lehranstalten Band II},
41 publisher = {Reniets Verlag},
43 note = {Schulbuch-Nr. 1682},
47 (* Compiler.Control.Print.printDepth:=5; (*4 default*)
50 refine fmz ["univariate","equation"];
52 "---- rlang.sml begin-----------------------------------";
53 (*----------------- Schalk I s.86 Bsp 5 ------------------------*)
54 "Schalk I s.86 Bsp 5 (3*x - 1 - (5*x - (2 - 4*x)) = -11)";
55 "Schalk I s.86 Bsp 5 (3*x - 1 - (5*x - (2 - 4*x)) = -11)";
56 "Schalk I s.86 Bsp 5 (3*x - 1 - (5*x - (2 - 4*x)) = -11)";
58 val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)",
59 "solveFor x","solutions L"];
60 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
63 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
64 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
65 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
66 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
67 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
68 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
69 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
70 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
71 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
72 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
73 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
74 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
75 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
77 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
78 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
79 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
80 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
81 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()
82 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 5 [x = 2]";
84 (*----------------- Schalk I s.86 Bsp 19 ------------------------*)
85 "Schalk I s.86 Bsp 19 (x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20)";
86 "Schalk I s.86 Bsp 19 (x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20)";
87 "Schalk I s.86 Bsp 19 (x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20)";
89 val fmz = ["equality ((x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20))",
90 "solveFor x","solutions L"];
91 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
94 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
95 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
96 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
97 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
98 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
99 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
100 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
101 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
102 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
103 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
104 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
105 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
106 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
107 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
108 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
109 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
110 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
111 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8]")) => ()
112 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 19 [x = 8]";
114 (*----------------- Schalk I s.86 Bsp 23 ------------------------*)
115 "Schalk I s.86 Bsp 19 ((2*x+5)^^^2+(3*x+4)^^^2=(13*x+2)*(x+1)+2*(15+14*x))";
116 "Schalk I s.86 Bsp 19 ((2*x+5)^^^2+(3*x+4)^^^2=(13*x+2)*(x+1)+2*(15+14*x))";
117 "Schalk I s.86 Bsp 19 ((2*x+5)^^^2+(3*x+4)^^^2=(13*x+2)*(x+1)+2*(15+14*x))";
119 val fmz = ["equality ((2*x+5)^^^2+(3*x+4)^^^2=(13*x+2)*(x+1)+2*(15+14*x))",
120 "solveFor x","solutions L"];
121 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
124 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
125 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
126 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
127 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
128 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
129 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
130 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
131 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
132 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
133 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
134 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
135 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
136 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
137 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
138 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
139 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
140 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
141 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -9]")) => ()
142 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 23 [x = -9]";
144 (*----------------- Schalk I s.86 Bsp 25 ------------------------*)
145 "Schalk I s.86 Bsp 25 ((2*x+1)^^^3+(x+1)^^^3=(2*x+1)^^^2*2*x+(x+2)^^^3+x^^^2)";
146 "Schalk I s.86 Bsp 25 ((2*x+1)^^^3+(x+1)^^^3=(2*x+1)^^^2*2*x+(x+2)^^^3+x^^^2)";
147 "Schalk I s.86 Bsp 25 ((2*x+1)^^^3+(x+1)^^^3=(2*x+1)^^^2*2*x+(x+2)^^^3+x^^^2)";
149 val fmz = ["equality ((2*x+1)^^^3+(x+1)^^^3=(2*x+1)^^^2*2*x+(x+2)^^^3+x^^^2)",
150 "solveFor x","solutions L"];
151 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
154 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
155 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
156 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
157 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
158 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
159 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
160 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
161 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
162 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
163 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
164 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
165 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
166 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
167 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
168 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
169 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
170 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
171 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -6 / 5]")) => ()
172 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 25 [x = -6 / 5]";
174 (*----------------- Schalk I s.86 Bsp 28b ------------------------*)
175 "Schalk I s.86 Bsp 28b ((3*x+5)/18 - x/2 = -((3*x - 2)/9))";
176 "Schalk I s.86 Bsp 28b ((3*x+5)/18 - x/2 = -((3*x - 2)/9))";
177 "Schalk I s.86 Bsp 28b ((3*x+5)/18 - x/2 = -((3*x - 2)/9))";
179 val fmz = ["equality ((3*x+5)/18 - x/2 = -((3*x - 2)/9))",
180 "solveFor x","solutions L"];
181 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
182 (*val p = e_pos'; val c = [];
183 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
184 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
185 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
186 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
187 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
188 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
189 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
190 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
191 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
192 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
193 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
194 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
195 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
196 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
197 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
198 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
199 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
200 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 28b []";
203 val bdv= (term_of o the o (parse thy)) "bdv";
204 val v = (term_of o the o (parse thy)) "x";
205 val t = (term_of o the o (parse thy)) "3 * x / 5";
206 val SOME (t',_) = rewrite_set_inst_ PolyEq.thy true
207 [(bdv, v)] make_ratpoly_in t;
208 if term2str t' = "3 / 5 * x" then () else raise error "rlang.sml: 1";
210 val t = str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
211 val subst = [(str2term "bdv", str2term "x")];
212 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
213 if term2str t' = "1 / 18 = 0" then () else raise error "rlang.sml: 2";
216 (*----------------- Schalk I s.87 Bsp 36b ------------------------*)
217 "Schalk I s.87 Bsp 36b ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 -(9*x- 7)/4 = 0)";
218 "Schalk I s.87 Bsp 36b ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 -(9*x- 7)/4 = 0)";
219 "Schalk I s.87 Bsp 36b ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 -(9*x- 7)/4 = 0)";
221 val fmz = ["equality ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0)",
222 "solveFor x","solutions L"];
223 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
226 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
227 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
228 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
229 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
230 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
231 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
232 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
233 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
234 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
235 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
236 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
237 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
238 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
239 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
240 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
241 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
242 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -237 / 65]")) => ()
243 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 36b [x = -237 / 65]";
247 val t = str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
248 val subst = [(str2term "bdv", str2term "x")];
249 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
251 if term2str t' = "79 / 12 + 65 / 36 * x = 0" then ()
252 else raise error "rlang.sml: 3";
256 (*----------------- Schalk I s.87 Bsp 38b ------------------------*)
257 "Schalk I s.87 Bsp 38b (-(2/x) + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) =65/8)";
258 "Schalk I s.87 Bsp 38b (-(2/x) + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) =65/8)";
259 "Schalk I s.87 Bsp 38b (-(2/x) + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) =65/8)";
261 val fmz = ["equality (-2/x + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) = 65/8)",
262 "solveFor x","solutions L"];
263 val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
266 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
267 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
268 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
269 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
270 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
271 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
272 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
273 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
274 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
275 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
276 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
277 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
278 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
279 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
280 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
281 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "296 + -3900 * x = 0")) then ()
282 else raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 38b";
283 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
284 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
285 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
286 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
287 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
288 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
289 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
290 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
291 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
292 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
293 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 74 / 975]")) => ()
294 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 38b [x = 74 / 975]";
296 (*----------------- Schalk I s.87 Bsp 40b ------------------------*)
297 "Schalk I s.87 Bsp 40b ((x+3)/(2*x - 4)=3)";
298 "Schalk I s.87 Bsp 40b ((x+3)/(2*x - 4)=3)";
299 "Schalk I s.87 Bsp 40b ((x+3)/(2*x - 4)=3)";
301 val fmz = ["equality ((x+3)/(2*x - 4)=3)",
302 "solveFor x","solutions L"];
303 val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
306 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
307 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
308 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
309 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
310 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
311 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
312 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
313 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
314 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
315 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
316 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
317 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
318 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
319 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
320 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
321 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
322 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;*)
323 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "15 + -5 * x = 0")) then ()
324 else raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 40b";
325 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
326 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
327 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
328 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
329 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
330 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
331 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
332 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
333 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
334 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 3]")) => ()
335 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 40b [x = 3]";
338 (*----------------- Schalk I s.87 Bsp 44a ------------------------*)
339 "Schalk I s.87 Bsp 44a ((1/2+(5*x)/2)^^^2 -((13*x)/2- 5/2)^^^2 -(6*x)^^^2+29)";
340 "Schalk I s.87 Bsp 44a ((1/2+(5*x)/2)^^^2 -((13*x)/2- 5/2)^^^2 -(6*x)^^^2+29)";
341 "Schalk I s.87 Bsp 44a ((1/2+(5*x)/2)^^^2 -((13*x)/2- 5/2)^^^2 -(6*x)^^^2+29)";
343 val fmz = ["equality ((1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 = -1*(6*x)^^^2 + 29)",
344 "solveFor x","solutions L"];
345 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
348 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
349 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
350 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
351 (*trace_rewrite:=true;
353 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
354 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
355 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
356 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
357 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
358 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
359 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
360 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
361 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
362 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
363 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
364 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
365 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
366 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
367 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1]")) => ()
368 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 44a [x = 1]";
371 val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 - (6*x)^^^2 + 29";
372 val subst = [(str2term "bdv", str2term "x")];
373 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
374 if term2str t' = "23 + 35 * x + -72 * x ^^^ 2" then ()
375 else raise error "rlang.sml: 4";
377 val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 + (6*x)^^^2 - 29";
378 val subst = [(str2term "bdv", str2term "x")];
379 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
380 if term2str t' = "-35 + 35 * x" then ()
381 else raise error "rlang.sml: 4.1";
384 (*----------------- Schalk I s.87 Bsp 52a ------------------------*)
385 "Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";
386 "Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";
387 "Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";
389 val fmz = ["equality ((5*x)/(x - 2) - x/(x+2)=4)",
390 "solveFor x","solutions L"];
391 val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
392 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
393 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
394 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
395 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
396 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
397 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
398 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
399 (*"12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)",Subproblem["normalize", "poly*)
400 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
401 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
402 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
403 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
404 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
405 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
406 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "16 + 12 * x = 0")) then ()
407 else raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 52a";
408 (*Subproblem["degree_1", "polynomial", "univariate", "equation"]*)
409 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
410 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
411 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
412 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
413 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
414 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
415 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
416 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
417 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
418 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -4 / 3]")) => ()
419 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 52a [x = -4 / 3]";
421 (*----------------- Schalk I s.87 Bsp 55b ------------------------*)
422 "Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)";
423 "Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)";
424 "Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)";
426 val fmz = ["equality (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)",
427 "solveFor x","solutions L"];
428 val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
429 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
430 (*val nxt = ("Model_Problem",Model_Problem["rational","univariate","equation"*)
431 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
432 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
433 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
434 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
435 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
436 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
437 (*//me's dropped !val it = ["9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3 ~= 0","x ~= 0"]
438 "(3 + -1 * x + 1 * x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + 1 * x ^^^3)"))
439 WN: Grad hoeher ~~~~~~~~~~~~ als notwendig ~~~~~~~~*)
440 (* nxt =Model_Problem ["normalize","polynomial","univariate","equation"])*)
441 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
442 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
443 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
444 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
445 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
446 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
447 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; 040209 MGs norm_Rational*)
448 (* val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])*)
449 if f= Form' (FormKF (~1, EdUndef, 0, Nundef, "-6 * x + 5 * x ^^^ 2 = 0"))then()
450 else raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b";
451 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
452 (*nxt=Model_Problem["bdv_only","degree_2","polynomial","univariate","equation*)
453 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
454 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
455 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
456 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
457 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
458 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
459 (*val f = Form' (FormKF (~1,EdUndef,3,Nundef,"x = 0 | x = 6 / 5")) : mout
460 val nxt = ("Or_to_List",Or_to_List) *)
461 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
462 (*val f = Form' (FormKF (~1,EdUndef,3,Nundef,"[x = 0, x = 6 / 5]")) : mout
463 val nxt = ("Check_elementwise",Check_elementwise "Assumptions")
464 get_assumptions pt (fst p);
465 val it = [] : string list ... correct for this subproblem !*)
466 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
467 (*val p = ([6,5,5],Res) : pos'
468 val f = Form' (FormKF (~1,EdUndef,3,Nundef,"[x = 0, x = 6 / 5]")) : mout
469 nxt=Check_Postcond ["bdv_only","degree_2","polynomial","univariate","equation*)
470 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
471 (*val p = ([6,5],Res) : pos'
472 val f = Form' (FormKF (~1,EdUndef,2,Nundef,"[x = 0, x = 6 / 5]")) : mout
473 val nxt =Check_Postcond ["normalize","polynomial","univariate","equation"])*)
474 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
475 (*val p = ([6],Res) : pos'
476 val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = 0, x = 6 / 5]")) : mout
477 val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
478 val [(aaa,ppp)] = get_assumptions_ pt p;
479 if term2str aaa = "9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0" then ()
480 else raise error "rlang.sml: diff.behav. in I s.87 Bsp 55b [x = 6 / 5], asms";
481 (*WN060717 unintentionally changed some rls/ord while
482 completing knowl. for thes2file...
483 if term2str aaa = "9 * x + (x ^^^ 3 + -6 * x ^^^ 2) ~= 0" then ()
484 else raise error "rlang.sml: diff.behav. in I s.87 Bsp 55b [x = 6 / 5], asms";
485 .... but it became even better*)
488 val it = "9 * x + (x ^^^ 3 + -6 * x ^^^ 2) ~= 0" : string;
490 val it = ["9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3 ~= 0","x ~= 0"]
491 > val subs = [(str2term "x", str2term "0")];
492 > val pred = str2term "9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3 ~= 0 & x ~= 0";
493 > eval_true thy [subst_atomic subs pred] rateq_erls;
494 val it = false : bool
495 > val subs = [(str2term "x", str2term "6 / 5")];
496 > val pred = str2term "9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3 ~= 0 & x ~= 0";
497 > eval_true thy [subst_atomic subs pred] rateq_erls;
498 val it = true : bool*)
499 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
500 (*val p = ([7],Res) : pos'
501 val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = 6 / 5]")) : mout
502 val nxt =Check_Postcond ["rational","univariate","equation"]) *)
503 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
504 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 6 / 5]")) => ()
505 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
507 (*----------------- Schalk I s.88 Bsp 64c ------------------------*)
508 "Schalk I s.88 Bsp 64c (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)";
509 "Schalk I s.88 Bsp 64c (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)";
510 "Schalk I s.88 Bsp 64c (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)";
512 val fmz = ["equality (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)",
513 "solveFor x","solutions L"];
514 val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
516 (*val p = e_pos'; val c = [];
517 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
518 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
519 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
520 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
521 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
522 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
523 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
524 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
525 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
526 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
527 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
528 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
529 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
530 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
531 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
532 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-3 + -1 * x = 0")) then ()
533 else raise error "rlangsml: diff.behav. in Schalk I s.88 Bsp 64c";
534 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
535 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
536 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
537 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
538 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
539 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
540 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
541 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
542 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
543 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
544 case f of Form' (FormKF (_,_,0,_,"[x = -3]")) => ()
545 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.88 Bsp 64c [x = -3]";
547 (*----------------- Schalk I s.88 Bsp 79a (2) ------------------------*)
548 "Schalk I s.88 Bsp 79a (2) (m1*v1+m2*v2=0)";
549 "Schalk I s.88 Bsp 79a (2) (m1*v1+m2*v2=0)";
550 "Schalk I s.88 Bsp 79a (2) (m1*v1+m2*v2=0)";
552 val fmz = ["equality (m1*v1+m2*v2=0)",
553 "solveFor m1","solutions L"];
554 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
556 (*val p = e_pos'; val c = [];
557 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
558 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
559 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
560 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
561 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
562 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
563 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
564 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
565 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
566 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
567 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
568 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
569 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
570 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
571 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
572 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
573 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[m1 = -1 * m2 * v2 / v1]")) => ()
574 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.88 Bsp 79a (2) [m1 = -1 * m2 * v2 / v1]";
576 (*----------------- Schalk I s.89 Bsp 90a(1) ------------------------*)
577 "Schalk I s.89 Bsp 90a (1) (f=((w+u)/(w+v))*v0)";
578 "Schalk I s.89 Bsp 90a (1) (f=((w+u)/(w+v))*v0)";
579 "Schalk I s.89 Bsp 90a (1) (f=((w+u)/(w+v))*v0)";
581 val fmz = ["equality (f=((w+u)/(w+v))*v0)",
582 "solveFor v","solutions L"];
583 val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
585 (*val p = e_pos'; val c = [];
586 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
587 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
588 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
589 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
590 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
591 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
592 (*val nxt = Specify_Problem ["rational","univariate","equation"]) *)
593 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
594 (*val nxt = Specify_Method ["RatEq","solve_rat_equation"]) *)
595 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
596 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
597 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
598 (*nxt = Subproblem ("RatEq.thy",["univariate","equation"])) *)
599 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
600 (*val nxt =Model_Problem ["normalize","polynomial","univariate","equation"])*)
601 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
602 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
603 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
604 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
605 (*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalize_poly"])*)
606 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
607 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
608 (*val nxt =Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
615 "f * w + -1 * u * v0 + -1 * v0 * w + f * v = 0")) then ()
616 else raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a";
617 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
618 (*val nxt = Model_Problem ["degree_1","polynomial","univariate","equation"])*)
619 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
620 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
621 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
622 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
623 (*val nxt = ("Apply_Method",Apply_Method ["PolyEq","solve_d1_poly_equation"])*)
624 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
625 (*val f = "v = -1 * (f * w + -1 * u * v0 + -1 * v0 * w) / f")) : mout
626 val nxt = ("Or_to_List",Or_to_List) : string * tac *)
627 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
628 (*val f = "[v = -1 * (f * w + -1 * u * v0 + -1 * v0 * w) / f]")) : mout
629 val nxt = ("Check_elementwise",Check_elementwise "Assumptions") *)
630 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
631 (*val f = "[v = -1 * (f * w + -1 * u * v0 + -1 * v0 * w) / f]")) : mout
632 val nxt = Check_Postcond ["degree_1","polynomial","univariate","equation"])*)
633 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
634 (*val f = "[v = -1 * (f * w + -1 * u * v0 + -1 * v0 * w) / f]")) : mout
635 val nxt = Check_Postcond ["normalize","polynomial","univariate","equation"])*)
636 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
637 (*val f = "[v = -1 * (f * w + -1 * u * v0 + -1 * v0 * w) / f]")) : mout
638 val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
640 get_assumptions_ pt p;
641 (*it = ["v + w ~= 0"] ... goes to the solution as an assumption*)
643 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
644 (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[]")) : mout
645 val nxt = Check_Postcond ["rational","univariate","equation"]) *)
646 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
647 case f of Form' (FormKF (~1,EdUndef,0,Nundef,
648 "[v = (u * v0 + v0 * w + -1 * f * w) / f]")) => ()
649 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a (1) [v=...]";
650 if get_assumptions_ pt p =
651 [(str2term"(u * v0 + v0 * w + -1 * f * w) / f + w ~= 0",[])] then ()
652 else raise error "rlang.sml: diff.behav. in I s.89 Bsp 90a (1) [v=...] asm";
655 (*----------------- Schalk I s.89 Bsp 90a(2) ------------------------*)
656 "Schalk I s.89 Bsp 90a (2) (f=((w+u)/(w+v))*v0)";
657 "Schalk I s.89 Bsp 90a (2) (f=((w+u)/(w+v))*v0)";
658 "Schalk I s.89 Bsp 90a (2) (f=((w+u)/(w+v))*v0)";
660 val fmz = ["equality (f=((w+u)/(w+v))*v0)",
661 "solveFor w","solutions L"];
662 val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
663 (*val p = e_pos';val c = [];
664 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
665 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
666 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
667 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
668 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
669 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
670 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
671 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
672 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
673 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
674 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
675 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
676 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
677 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
684 "f * v + -1 * u * v0 + (f + -1 * v0) * w = 0")) then ()
685 else raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a (2)";
686 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
687 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
688 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
689 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
690 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
691 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
692 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
693 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
694 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
695 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[w = (u * v0 + -1 * f * v) / (f + -1 * v0)]")) => ()
696 | _ => raise error "rlang.sml: diff.behav. in Schalk I Bsp 90a(2)";
697 if get_assumptions_ pt p =
698 [(str2term"v + (u * v0 + -1 * f * v) / (f + -1 * v0) ~= 0",[]),
699 (str2term"f + -1 * v0 ~= 0",[])]
700 then writeln "asm should be simplified ???"
701 else raise error "rlang.sml: diff.behav. in Schalk I Bsp 90a(2) asm";
703 (*----------------- Schalk I s.89 Bsp 98a(1) ------------------------*)
704 "Schalk I s.89 Bsp 98a (1) (1/R=1/R1+1/R2)";
705 "Schalk I s.89 Bsp 98a (1) (1/R=1/R1+1/R2)";
706 "Schalk I s.89 Bsp 98a (1) (1/R=1/R1+1/R2)";
708 val fmz = ["equality (1/R=1/R1+1/R2)",
709 "solveFor R1","solutions L"];
710 val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
711 (*val p = e_pos'; val c = [];
712 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
713 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
714 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
715 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
716 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
717 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
718 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
719 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
720 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
721 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
722 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
723 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
724 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
725 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
726 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
729 (~1, EdUndef, 0, Nundef, "-1 * R * R2 + (R2 + -1 * R) * R1 = 0"))then()
730 else raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 98a (1)";
731 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
732 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
733 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
734 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
735 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
736 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
737 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
738 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
739 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
740 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[R1 = R * R2 / (R2 + -1 * R)]")) => ()
741 | _ => raise error "rlang.sml: diff.behav. in 98a(1) [R1 = ...]";
742 if get_assumptions_ pt p = [(str2term"R * R2 * R2 ~= (R2 + -1 * R) * 0",[]),
743 (str2term"R2 + -1 * R ~= 0",[]),
744 (str2term"R2 + -1 * R ~= 0",[])]
745 then writeln "asm should be simplified"
746 else raise error "rlang.sml: diff.behav. in 98a(1) asm";
748 (*----------------- Schalk I s.89 Bsp 104a(1) ------------------------*)
749 "Schalk I s.89 Bsp 104a (1) (y^^^2=2*p*x)";
750 "Schalk I s.89 Bsp 104a (1) (y^^^2=2*p*x)";
751 "Schalk I s.89 Bsp 104a (1) (y^^^2=2*p*x)";
752 (*ER-13 + EO-11 ?!?*)
753 val fmz = ["equality (y^^^2=2*p*x)",
754 "solveFor p","solutions L"];
755 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
756 (*val p = e_pos'; val c = [];
757 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
758 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
759 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
760 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
761 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
762 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
763 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
764 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
765 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
766 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
767 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
768 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
769 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
770 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
771 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
772 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
773 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
774 case f of Form' (FormKF (_,_,0,_,"[p = y ^^^ 2 / (2 * x)]")) => ()
775 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 104a (1) [p = y^2/(2*x)]";
776 if get_assumptions_ pt p = [(str2term"-2 * x ~= 0",[])]
777 then writeln"should be x ~= 0\nshould be x ~= 0\nshould be x ~= 0\n"
778 else raise error "rlang.sml: diff.behav. in I s.89 Bsp 104a(1) asm";
781 (*----------------- Schalk I s.89 Bsp 104a(2) ------------------------*)
782 "Schalk I s.89 Bsp 104a (2) (y^^^2=2*p*x)";
783 "Schalk I s.89 Bsp 104a (2) (y^^^2=2*p*x)";
784 "Schalk I s.89 Bsp 104a (2) (y^^^2=2*p*x)";
786 val fmz = ["equality (y^^^2=2*p*x)",
787 "solveFor y","solutions L"];
788 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
791 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
792 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
793 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
794 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
795 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
796 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
797 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
798 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
799 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
800 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
801 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
802 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
803 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
804 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
805 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
806 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
807 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
808 case f of Form' (FormKF (_,_,0,_,"[y = sqrt (2 * p * x), y = -1 * sqrt (2 * p * x)]")) => ()
809 | _ => raise error "rlang.sml: diff.behav. Schalk I s.89 Bsp 104a(2) [x = ]";
810 if get_assumptions_ pt p = [(str2term"0 <= -1 * (-2 * p * x)",[]),(str2term"0 <= -1 * (-2 * p * x)",[])] then writeln "asm should be simplified\nshould be simplified"
811 else raise error "rlang.sml: diff.behav. in I s.89 Bsp 104a(2) asm";
814 (*----------------- Schalk I s.90 Bsp 118a (1) ------------------------*)
815 "Schalk I s.90 Bsp 118a (1) (b^^^2*x^^^2 + a^^^2*y^^^2 = a^^^2*b^^^2)";
816 "Schalk I s.90 Bsp 118a (1) (b^^^2*x^^^2 + a^^^2*y^^^2 = a^^^2*b^^^2)";
817 "Schalk I s.90 Bsp 118a (1) (b^^^2*x^^^2 + a^^^2*y^^^2 = a^^^2*b^^^2)";
819 val fmz = ["equality (b^^^2*x^^^2 + a^^^2*y^^^2 = a^^^2*b^^^2)",
820 "solveFor x","solutions L"];
821 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
824 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
825 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
826 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
827 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
828 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
829 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
831 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
832 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;
833 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;
834 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;
836 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
837 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
838 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
839 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
840 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
841 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
842 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
843 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
844 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;
845 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_asm (fst p, fst p) pt;
846 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_asm (fst p, fst p) pt;
847 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_asm (fst p, fst p) pt;
848 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_asm (fst p, fst p) pt;
849 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;asms2str (get_asm (fst p, fst p) pt);
850 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;asms2str (get_asm (fst p, fst p) pt);
852 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_asm (fst p, fst p) pt;
853 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_asm (fst p, fst p) pt;
854 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = sqrt ((a ^^^ 2 * b ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2) / b ^^^ 2),\n x = -1 * sqrt ((a ^^^ 2 * b ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2) / b ^^^ 2)]")) => writeln"should be simplified MG"
855 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) [x = ]";
856 val asms = get_assumptions_ pt p;
857 if asms = [(str2term"0 * b ^^^ 2 <= -1 * (a ^^^ 2 * y ^^^ 2 + -1 * a ^^^ 2 * b ^^^ 2)", []),
858 (str2term"b ^^^ 2 ~= 0", []),
859 (str2term"0 * b ^^^ 2 <= -1 * (a ^^^ 2 * y ^^^ 2 + -1 * a ^^^ 2 * b ^^^ 2)", []),
860 (str2term"b ^^^ 2 ~= 0", [])
861 ] then writeln"should be simplified MG"
862 else raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) asms";
864 (*----------------- Schalk I s.102 Bsp 268(1) ------------------------*)
865 "Schalk I s.102 Bsp 268(1) (A = (1/2)*(x1*(y2-y3)+x2*(y3 - y1)+x3*(y1 - y2)))";
866 "Schalk I s.102 Bsp 268(1) (A = (1/2)*(x1*(y2-y3)+x2*(y3 - y1)+x3*(y1 - y2)))";
867 "Schalk I s.102 Bsp 268(1) (A = (1/2)*(x1*(y2-y3)+x2*(y3 - y1)+x3*(y1 - y2)))";
869 val fmz = ["equality (A = (1/2)*(x1*(y2 - y3)+x2*(y3 - y1)+x3*(y1 - y2)))",
870 "solveFor x2","solutions L"];
871 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
874 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
875 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
876 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
877 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
878 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
879 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
880 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
881 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
882 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
883 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
884 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
885 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
886 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
887 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
888 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
889 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
890 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
891 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x2 =\n (-2 * A + x1 * y2 + x3 * y1 + -1 * x1 * y3 + -1 * x3 * y2) /\n (y1 + -1 * y3)]")) => ()
892 | _ => raise error "rlang.sml: diff.behav. Schalk I s.102 Bsp 268(1) [x2=...]";
893 if get_assumptions_ pt p = [(str2term"y1 / 2 + -1 * y3 / 2 ~= 0",[])] then ()
894 else raise error "rlang.sml: diff.behav. in I s.102 Bsp 268(1) asm";
896 (*-------------------- Schalk II ----------------------------*)
897 (*-------------------- Schalk II ----------------------------*)
898 (*-------------------- Schalk II ----------------------------*)
899 (*-------------------- Schalk II ----------------------------*)
900 (*-------------------- Schalk II ----------------------------*)
903 (*----------------- Schalk II s.56 Bsp 67b ------------------------*)
904 "Schalk II s.56 Bsp 67b (4*sqrt(4*x+1)=3*sqrt(7*x+2))";
905 "Schalk II s.56 Bsp 67b (4*sqrt(4*x+1)=3*sqrt(7*x+2))";
906 "Schalk II s.56 Bsp 67b (4*sqrt(4*x+1)=3*sqrt(7*x+2))";
908 val fmz = ["equality (4*sqrt(4*x+1)=3*sqrt(7*x+2))",
909 "solveFor x","solutions L"];
910 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
913 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
914 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
915 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
916 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
917 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
918 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
919 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
920 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
921 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
922 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
923 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
924 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
925 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
926 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
927 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
928 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-2 + x = 0")) then ()
929 else raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 67b";
930 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
931 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
932 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
933 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
934 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
935 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
936 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
937 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
938 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
939 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()
940 | _ => raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 67b [x=2]";
942 (*----------------- Schalk II s.56 Bsp 68a ------------------------*)
943 "Schalk II s.56 Bsp 68a (5*sqrt(x) - 1 = 7*sqrt(x) - 5)";
944 "Schalk II s.56 Bsp 68a (5*sqrt(x) - 1 = 7*sqrt(x) - 5)";
945 "Schalk II s.56 Bsp 68a (5*sqrt(x) - 1 = 7*sqrt(x) - 5)";
946 val fmz = ["equality (5*sqrt(x) - 1 = 7*sqrt(x) - 5)",
947 "solveFor x","solutions L"];
948 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
951 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
952 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
953 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
954 (* val nxt = ("Model_Problem",Model_Problem ["normalize","root","univariate","equation"])*)
955 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
956 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
957 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
958 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
959 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
960 (* val nxt = ("Model_Problem",Model_Problem ["sq","root","univariate","equation"]) *)
961 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
962 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
963 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
964 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
965 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
966 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
967 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
968 (* val nxt = ("Model_Problem",Model_Problem ["sq","root","univariate","equation"]) *)
969 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
970 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
971 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
972 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
973 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
974 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
975 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
976 get_assumptions_ pt p;
977 (* val nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*)
978 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
979 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
980 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
981 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
982 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
985 (~1, EdUndef, 0, Nundef, "256 + -2368 * x + 576 * x ^^^ 2 = 0"))then()
986 else raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 68a";
987 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
988 get_assumptions_ pt p;
989 (* val nxt = ("Model_Problem", Model_Problem
990 ["abcFormula","degree_2","polynomial","univariate","equation"])*)
991 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
992 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
993 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
994 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
995 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
996 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
997 get_assumptions_ pt p;
998 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
999 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1000 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1001 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1002 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4, x = 1 / 9]"))
1003 then writeln "only [x = 4] !\nonly [x = 4] !\nonly [x = 4] !\n"
1004 else raise error "rlang.sml: diff.behav. in II 68a";
1005 val asms = get_assumptions_ pt p;
1007 "[(0 <= (25 * (1 / 9) + -1 * (16 + 49 * (1 / 9))) * -56, []),\
1010 \(0 <= (-5 + 7 * sqrt (1 / 9) + 1) * 5, []),\
1012 \(0 <= (25 * (1 / 9) + -1 * (16 + 49 * (1 / 9))) * -56, []),\
1014 (*WN050916 before correction 'rewrite__set_ called with 'Erls' for ..'
1015 thus: maybe the rls for the asms is Erls ??:
1016 [(str2term"0 <= (25 * (1 / 9) + -1 * (16 + 49 * (1 / 9))) * -56", []),
1017 (str2term"9 ~= 0", []),
1018 (str2term"0 <= (-5 + 7 * sqrt (1 / 9) + 1) * 5", []),
1019 (str2term"9 ~= 0", []),
1020 (str2term"0 <= (25 * (1 / 9) + -1 * (16 + 49 * (1 / 9))) * -56", [])]*)
1021 then "should get True * False!!!"
1022 else raise error "rlang.sml: diff.behav. in II 68a asms";
1024 (*----------------- Schalk II s.56 Bsp 73b ------------------------*)
1025 "Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
1026 "Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
1027 "Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
1029 val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))",
1030 "solveFor x","solutions L"];
1031 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1033 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1034 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1035 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1036 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1037 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1038 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1039 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1040 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1041 (*"13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"
1042 -> Subproblem ("RootEq.thy", ["univariate", ...])*)
1043 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1044 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1045 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1046 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1047 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1048 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1049 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1050 (*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"
1051 -> Subproblem ("RootEq.thy", ["univariate", ...])*)
1052 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1053 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1054 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1055 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1056 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1057 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1058 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
1059 else raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 73b";
1060 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1061 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1062 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1063 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1064 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1065 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1066 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1067 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1068 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1069 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1070 val asm = get_assumptions_ pt p;
1071 if asm=[] andalso f = Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) andalso nxt = ("End_Proof'",End_Proof') then ()
1072 else raise error "rlang.sml: diff.behav. in UniversalList 2";
1074 (*----------------- Schalk II s.56 Bsp 74a ------------------------*)
1075 "Schalk II s.56 Bsp 74a (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))";
1076 "Schalk II s.56 Bsp 74a (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))";
1077 "Schalk II s.56 Bsp 74a (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))";
1079 val fmz = ["equality (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))",
1080 "solveFor x","solutions L"];
1081 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1083 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1084 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1085 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1086 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1087 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1088 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1089 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1090 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1091 (*4 + 5 * x + -2 * sqrt (3 + 13 * x + 4 * x ^^^ 2) = -2 + x"
1092 -> Subproblem ("RootEq.thy", ["univariate", ...])*)
1093 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1094 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1095 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1096 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1097 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1098 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1099 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1100 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1101 (*"12 + 52 * x + 16 * x ^^^ 2 = 36 + x ^^^ 2 + 48 * x + 15 * x ^^^ 2"
1102 -> Subproblem ("RootEq.thy", ["univariate", ...])*)
1103 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1104 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1105 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1106 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1107 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1108 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1109 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-24 + 4 * x = 0")) then ()
1110 else raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 74a";
1111 (*-> ubproblem ("PolyEq.thy", ["degree_1", ...]*)
1112 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1113 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1114 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1115 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1121 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1122 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 6]")) => ()
1123 | _ => raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 74a [x = 6]";
1126 (*----------------- Schalk II s.56 Bsp 77b ------------------------*)
1127 "Schalk II s.56 Bsp 77b (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))";
1128 "Schalk II s.56 Bsp 77b (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))";
1129 "Schalk II s.56 Bsp 77b (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))";
1131 val fmz = ["equality (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))",
1132 "solveFor x","solutions L"];
1133 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1135 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1136 (* val nxt = ("Model_Problem",Model_Problem ["sq","root","univariate","equation"]) *)
1137 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1138 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1139 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1140 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1141 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1142 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1143 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1144 (* val nxt = ("Model_Problem",Model_Problem ["sq","root","univariate","equation"]) *)
1145 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1146 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1147 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1148 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1149 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1150 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1151 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
1152 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1153 (* val nxt = ("Model_Problem",Model_Problem ["sq","root","univariate","equation"]) *)
1154 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1155 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1156 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1157 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1158 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1159 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1160 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1161 (*val nxt = ("Model_Problem",
1162 Model_Problem ["normalize","polynomial","univariate","equation"])*)
1163 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1164 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1165 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1166 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1167 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1168 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; since MGs norm_Rational*)
1169 if f = Form'(FormKF (~1, EdUndef, 0, Nundef, "451584 + -112896 * x = 0"))then()
1170 else raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 77b";
1171 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1172 (* val nxt = ("Model_Problem",
1173 Model_Problem ["degree_1","polynomial","univariate","equation"])*)
1174 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1175 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1176 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1177 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1178 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1179 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1180 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1181 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1182 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1183 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
1184 | _ => raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 77b []";
1185 (*added 040209 at introducing MGs norm_Rational ?!*)
1186 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1189 (*----------------- Schalk II s.66 Bsp 4 ------------------------*)
1190 "Schalk II s.66 Bsp 4 ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)";
1191 "Schalk II s.66 Bsp 4 ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)";
1192 "Schalk II s.66 Bsp 4 ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)";
1194 val fmz = ["equality ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)",
1195 "solveFor x","solutions L"];
1196 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1199 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1200 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1201 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1202 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1203 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1204 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1205 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1206 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1207 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1208 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1209 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1210 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1211 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1212 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1213 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1214 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1215 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1216 case f of Form' (FormKF (_,_,0,_,"[x = 5, x = -5]")) => ()
1217 | _ => raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 4 []";
1220 (*----------------- Schalk II s.66 Bsp 8a ------------------------*)
1221 "Schalk II s.66 Bsp 8a ((x - 4)/(x+4) = (1 - x)/(1+x))";
1223 val fmz = ["equality ((x - 4)/(x+4) = (1 - x)/(1+x))",
1224 "solveFor x","solutions L"];
1225 val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
1227 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1228 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1229 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1230 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1231 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1232 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1233 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1234 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
1235 (*"(-4 + x) * (1 + x) = (1 + -1 * x) * (4 + x)"
1236 -> Subproblem ("RatEq.thy", ["univariate", ...])*)
1237 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1238 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1239 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1240 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1241 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1242 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1243 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1244 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-8 + 2 * x ^^^ 2 = 0")) then ()
1245 else raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 8a";
1246 (*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*)
1248 val Form' (FormKF (~1, EdUndef, 0, Nundef, str)) = f;
1250 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1251 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1252 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1253 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1254 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1255 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1256 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1257 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1258 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1259 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
1260 | _ => raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 8a [x = 2, x = -2]";
1262 (*----------------- Schalk II s.66 Bsp 10b ------------------------*)
1263 "Schalk II s.66 Bsp 10b (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))";
1264 "Schalk II s.66 Bsp 10b (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))";
1265 "Schalk II s.66 Bsp 10b (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))";
1266 val fmz = ["equality (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))",
1267 "solveFor x","solutions L"];
1268 val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
1271 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1272 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1273 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1274 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1275 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1276 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1277 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1278 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1279 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1280 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1281 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1282 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1283 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1284 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1285 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1292 "60 + 28 * x + -13 * x ^^^ 2 + -1 * x ^^^ 3 = 0")) then ()
1293 else raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 10b";
1294 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1295 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1296 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1297 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1298 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1299 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1300 (*60 + 28 * x + -13 * x ^^^ 2 + -1 * x ^^^ 3 = 0 ... degree 3 not solvable*)
1303 (*----------------- Schalk II s.66 Bsp 20a ------------------------*)
1305 "Schalk II s.66 Bsp 20a (sqrt(29 - sqrt (x^^^2 - 9))=5)";
1306 "Schalk II s.66 Bsp 20a (sqrt(29 - sqrt (x^^^2 - 9))=5)";
1307 "Schalk II s.66 Bsp 20a (sqrt(29 - sqrt (x^^^2 - 9))=5)";
1308 val fmz = ["equality (sqrt(29 - sqrt(x^^^2 - 9))=5)",
1309 "solveFor x","solutions L"];
1310 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1313 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1314 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1315 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1316 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1317 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1318 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1319 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1320 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1321 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1322 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1323 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1324 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1325 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1326 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1327 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1328 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1329 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1330 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1331 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1332 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1333 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1334 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-25 + x ^^^ 2 = 0")) then ()
1335 else raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 20a";
1336 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1337 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1338 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1339 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1340 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1341 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1342 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1343 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1344 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1345 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1346 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1347 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 5, x = -5]")) => ()
1348 | _ => raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 20a [x = 5, x = -5]";
1350 (*----------------- Schalk II s.66 Bsp 23b ------------------------*)
1351 "Schalk II s.66 Bsp 23b (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))";
1352 "Schalk II s.66 Bsp 23b (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))";
1353 "Schalk II s.66 Bsp 23b (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))";
1354 (*EO WN060310 something wrong:
1355 ([6, 6, 3, 1], Frm) "-1064944 + 32 * x + -48 * x ^^^ 2 = 0"
1357 ([6, 6, 3, 1], Res) "False"
1359 val fmz = ["equality (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))",
1360 "solveFor x","solutions L"];
1361 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1363 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1364 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1365 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1366 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1367 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1368 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1369 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1370 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1371 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1372 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1373 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1374 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1375 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1376 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1377 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1378 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1379 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1380 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1381 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1382 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1383 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
1386 (~1, EdUndef, 0, Nundef, "-1064944 + 32 * x + -48 * x ^^^ 2 = 0"))then()
1387 else raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 23b";
1388 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1389 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1390 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1391 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1392 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1393 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1394 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1395 case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[]")) => ()
1396 | _ => raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 23b []";
1398 (*----------------- Schalk II s.66 Bsp 28a ------------------------*)
1399 "Schalk II s.66 Bsp 28a (A=(c/d)*sqrt(4*a^^^2 - c^^^2))";
1400 "Schalk II s.66 Bsp 28a (A=(c/d)*sqrt(4*a^^^2 - c^^^2))";
1401 "Schalk II s.66 Bsp 28a (A=(c/d)*sqrt(4*a^^^2 - c^^^2))";
1402 val fmz = ["equality (A=(c/d)*sqrt(4*a^^^2 - c^^^2))",
1403 "solveFor a","solutions L"];
1404 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1407 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1408 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1409 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1410 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1411 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1412 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1413 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1414 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1415 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1416 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1417 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1418 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1419 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1420 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1427 "c ^^^ 4 / d ^^^ 2 + A ^^^ 2 * d ^^^ 2 / d ^^^ 2 +\n-4 * c ^^^ 2 / d ^^^ 2 * a ^^^ 2 =\n0")) then ()*)
1429 "c ^^^ 4 / d ^^^ 2 + A ^^^ 2 / 1 + -4 * c ^^^ 2 / d ^^^ 2 * a ^^^ 2 = 0"
1430 then () else raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 28a";
1431 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1432 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1433 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1434 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1435 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1436 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1437 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1438 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1439 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1440 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[a = sqrt ((c ^^^ 4 + A ^^^ 2 * d ^^^ 2) / (4 * c ^^^ 2)),\n a = -1 * sqrt ((c ^^^ 4 + A ^^^ 2 * d ^^^ 2) / (4 * c ^^^ 2))]")) => ()
1441 | _ => raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 28a [a=...]";
1445 (*----------------- Schalk II s.68 Bsp 52b ------------------------*)
1446 "Schalk II s.68 Bsp 52b (1/(x - a+b)=1/x - 1/a + 1/b)";
1447 val fmz = ["equality (1/(x - a+b)=1/x - 1/a + 1/b)",
1448 "solveFor x","solutions L"];
1449 val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
1450 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1451 (* val nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"])*)
1452 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1453 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1454 (*val nxt = ("Specify_Theory",Specify_Theory "RatEq.thy")*)
1455 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1456 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1457 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1458 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1460 val f="1 * (a * (b * x)) = (a * b + (a * x + -1 * (b * x))) * (b + (x + -1 * a)
1461 val nxt = Subproblem ("RatEq.thy",["univariate","equation"]))*)
1462 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1463 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1464 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1465 (*val nxt = ("Specify_Theory",Specify_Theory "PolyEq.thy")*)
1466 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1467 (* nxt = Specify_Problem ["normalize","polynomial","univariate","equation"])*)
1468 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1469 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1470 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1471 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1472 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; at introducing of MGs norm_Rational*)
1473 (*val p = ([4,5],Res) val f ="b * a ^^^ 2 + -1 * a * b ^^^ 2 + (a ^^^ 2 + b ^^^ 2 + -2 * a * b) * x +\n(b + -1 * a) * x ^^^ 2 =\n0"))
1474 val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
1481 "b * a ^^^ 2 + -1 * a * b ^^^ 2 + (a ^^^ 2 + b ^^^ 2 + -2 * a * b) * x +\n(b + -1 * a) * x ^^^ 2 =\n0")) then ()
1482 else raise error "rlang.sml: diff.behav. in chalk I s.87 Bsp 38b";
1483 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1484 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1485 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1486 (*val nxt = ("Specify_Theory",Specify_Theory "PolyEq.thy")*)
1487 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1488 (*Specify_Problem["abcFormula","degree_2","polynomial","univariate","equation*)
1489 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1490 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1491 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1492 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1493 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1494 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;introducing MGs norm_Rational*)
1495 (*val p = ([4,6,5],Res) val f ="[x =\n (2 * a * b + -1 * a ^^^ 2 + -1 * b ^^^ 2 +\n sqrt\n (a ^^^ 4 + b ^^^ 4 + -4 * a * a * b ^^^ 2 + -4 * a * b * a ^^^ 2 +\n -4 * b * b * a ^^^ 2 +\n 4 * a * a * b ^^^ 2 +\n 4 * a * b * a ^^^ 2 +\n 2 * a ^^^ 2 * b ^^^ 2)) /\n (-2 * a + 2 * #"
1496 nx Check_Postcond["abcFormula","degree_2","polynomial","univariate","equation*)
1497 (*9.9.03: -"- ["normalize","polynomial","univar...*)
1498 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1499 (*val p = ([4,6],Res)
1500 val nxt =Check_Postcond ["normalize","polynomial","univariate","equation"])*)
1501 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1502 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*1 additional for MGs norm_Rational*)
1503 if p = ([],Res) andalso f = Form' (FormKF (~1,EdUndef,0,Nundef,
1504 "[x =\n (2 * a * b + -1 * a ^^^ 2 + -1 * b ^^^ 2 +\n sqrt\n (a ^^^ 4 + b ^^^ 4 + -4 * a * a * b ^^^ 2 + -4 * a * b * a ^^^ 2 +\n -4 * b * b * a ^^^ 2 +\n 4 * a * a * b ^^^ 2 +\n 4 * a * b * a ^^^ 2 +\n 2 * a ^^^ 2 * b ^^^ 2)) /\n (-2 * a + 2 * b),\n x =\n (2 * a * b + -1 * a ^^^ 2 + -1 * b ^^^ 2 +\n -1 *\n sqrt\n (a ^^^ 4 + b ^^^ 4 + -4 * a * a * b ^^^ 2 + -4 * a * b * a ^^^ 2 +\n -4 * b * b * a ^^^ 2 +\n 4 * a * a * b ^^^ 2 +\n 4 * a * b * a ^^^ 2 +\n 2 * a ^^^ 2 * b ^^^ 2)) /\n (-2 * a + 2 * b)]")) andalso nxt = ("End_Proof'",End_Proof') then writeln"simplify MG"
1505 else raise error "rlang.sml: diff.behav. in rational-a-b";
1507 (*----------------- Schalk II s.68 Bsp 56a ------------------------*)
1508 "Schalk II s.68 Bsp 56a ((a+b*x)/(a-b*x) - (a - b*x)/(a+b*x)= (4*a*b)/(a^^^2 - b^^^2))";
1509 val fmz = ["equality ((a+b*x)/(a-b*x) - (a - b*x)/(a+b*x)= (4*a*b)/(a^^^2 - b^^^2))","solveFor x","solutions L"];
1510 val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
1511 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1512 (* val nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"]) *)
1513 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1514 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1515 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1516 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1517 (*SK loops with poly:
1518 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1519 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1522 (a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) =
1523 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)
1524 common_nominator_p wird nicht angewendet, weil ...
1525 add_fract terminiert nicht: 030603
1526 siehe Rational.ML rational.sml
1530 "(a + b * x) / (a + -1 * (b * x)) + -1 * (a + -1 * (b * x)) / (a + b * x) =\n4 * a * b / (a ^^^ 2 + -1 * b ^^^ 2)"
1532 val nxt = ("Rewrite_Set",Rewrite_Set "make_ratpoly") : string * tac
1533 "(a + b * x) / (a + -1 * b * x) + (-1 * a + b * x) / (a + b * x) =\n4 *
1534 a * b / (a ^^^ 2 + -1 * b ^^^ 2)"
1537 val t = str2term"(a + b * x) / (a + -1 * (b * x)) + -1 * (a + -1 * (b * x)) / (a + b * x) =\n4 * a * b / (a ^^^ 2 + -1 * b ^^^ 2)";
1538 trace_rewrite:=true;
1539 val SOME (t',asm) = rewrite_set_ thy false norm_Rational t;
1541 trace_rewrite:=false;
1543 # rls: norm_Rational on: (a + b * x) / (a + -1 * (b * x)) + -1 * (a + -1 * (b * x)) / (a + b * x) = 4 * a * b / (a ^^^ 2 + -1 * b ^^^ 2)
1545 ## rls: discard_minus on:
1547 ## rls: rat_mult_divide on:
1549 ## rls: reduce_0_1_2 on:
1550 ## rls: order_add_mult on:
1551 ### try thm: real_mult_commute
1552 === rewrites to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + -1 * (-1 * (b * x))) / (a + b * x) = b * (4 * a) / (a ^^^ 2 + -1 * b ^^^ 2)
1554 ### try thm: real_mult_left_commute
1555 === rewrites to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + -1 * (-1 * (b * x))) / (a + b * x) = 4 * (b * a) / (a ^^^ 2 + -1 * b ^^^ 2)
1557 ### try thm: real_mult_commute
1558 === rewrites to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + -1 * (-1 * (b * x))) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)
1561 === calc. to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + 1 * (b * x)) / (a +b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)
1563 ## rls: common_nominator_p on: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + 1 * (b * x)) / (a + b * x) =
1564 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)
1565 !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!GC
1567 ## rls: discard_minus on:
1569 ## rls: rat_mult_divide on:
1571 ## rls: reduce_0_1_2 on:
1572 ### try thm: real_mult_1
1573 === rewrites to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)
1575 ## rls: order_add_mult on:
1577 ## rls: common_nominator_p on: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) =
1578 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)
1579 !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!GC
1581 ## rls: discard_minus on:
1583 ## rls: rat_mult_divide on:
1585 ## rls: reduce_0_1_2 on:
1586 ## rls: order_add_mult on:
1587 ## rls: collect_numerals on:
1588 ## rls: common_nominator_p on: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) =
1589 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)
1590 !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!GC
1594 (*----------------- Schalk II s.68 Bsp 61b ------------------------*)
1595 "Schalk II s.68 Bsp 61b (sqrt(x+a)+sqrt(b - x)=sqrt(a+b))";
1596 val fmz = ["equality (sqrt(x+a)+sqrt(b - x)=sqrt(a+b))",
1597 "solveFor x","solutions L"];
1598 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1600 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1601 (* val nxt = ("Model_Problem",Model_Problem ["sq","root","univariate","equation"])*)
1602 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1603 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1604 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1605 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1606 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1607 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1608 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1609 (* val nxt = ("Model_Problem",Model_Problem ["sq","root","univariate","equation"])*)
1610 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1611 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1612 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1613 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1614 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1615 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1616 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1617 (*val nxt = ("Model_Problem",
1618 Model_Problem ["normalize","polynomial","univariate","equation"])*)
1619 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1620 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1621 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1622 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1623 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1630 (*"-4 * b ^^^ 2 + -4 * a * b + 4 * b ^^^ 2 + 8 * a * b +\n(-2 * a + -4 * a + -4 * b + 2 * a + 8 * b) * x +\n-4 * x ^^^ 2 =\n0" before MG*)
1631 "4 * a * b + (-4 * a + 4 * b) * x + -4 * x ^^^ 2 = 0")) then ()
1632 else raise error "rlang.sml: diff.behav. in Schalk II s.68 Bsp 61b";
1633 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1634 (*val nxt = ("Model_Problem", Model_Problem
1635 ["abcFormula","degree_2","polynomial","univariate","equation"])*)
1636 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1637 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1638 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1639 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1640 (* f= ... "-4 * b ^^^ 2 + -4 * a * b + 4 * b ^^^ 2 + 8 * a * b +
1641 (-2 * a + -4 * a + -4 * b + 2 * a + 8 * b) * x + -4 * x ^^^ 2 =0"*)
1642 (*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"d2_polyeq_abcFormula_simplify"))*)
1643 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1644 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1645 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1646 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1647 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1648 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1649 (*if f = Form' (FormKF (~1,EdUndef,0,Nundef, with norm_Rational before MG
1650 "[x =\n (-2 * a + -4 * b + 6 * a +\n sqrt\n (32 * a * b + -16 * a ^^^ 2 + -48 * b ^^^ 2 + 24 * a ^^^ 2 +\n 64 * b ^^^ 2 +\n 8 * a ^^^ 2)) /\n -8,\n x =\n (-2 * a + -4 * b + 6 * a +\n -1 *\n sqrt\n (32 * a * b + -16 * a ^^^ 2 + -48 * b ^^^ 2 + 24 * a ^^^ 2 +\n 64 * b ^^^ 2 +\n 8 * a ^^^ 2)) /\n -8]")) then writeln"simplify MG"*)
1651 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x =\n (-4 * b + 4 * a + sqrt (32 * a * b + 16 * a ^^^ 2 + 16 * b ^^^ 2)) / -8,\n x =\n (-4 * b + 4 * a + -1 * sqrt (32 * a * b + 16 * a ^^^ 2 + 16 * b ^^^ 2)) /\n -8]")) then ()
1652 else raise error "rlang.sml: diff.behav. Bsp 61b";
1653 (*WN.18.12.03: extreme run-time !!!*)
1656 (*----------------- Schalk II s.68 Bsp 62b ------------------------*)
1657 "Schalk II s.68 Bsp 62b (sqrt((x+a)^^^2+(x - 2*b)^^^2)=a+2*b)";
1658 val fmz = ["equality (sqrt((x+a)^^^2+(x - 2*b)^^^2)=a+2*b)",
1659 "solveFor x","solutions L"];
1660 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1661 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1662 (*val nxt = ("Model_Problem",Model_Problem ["sq","root","univariate","equation"]) *)
1663 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1664 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1665 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1666 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1667 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1668 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1669 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1670 (* val nxt = ("Model_Problem",
1671 Model_Problem ["normalize","polynomial","univariate","equation"])*)
1672 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1673 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1674 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1675 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1676 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1683 "-4 * a * b + (-4 * b + 2 * a) * x + 2 * x ^^^ 2 = 0")) then ()
1684 else raise error "rlang.sml: diff.behav. in Schalk II s.68 Bsp 62b";
1685 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1686 (*val nxt = ("Model_Problem", Model_Problem
1687 ["abcFormula","degree_2","polynomial","univariate","equation"])*)
1688 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1689 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1690 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1691 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1692 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1693 (*val f = ... "-4 * a * b + (-4 * b + 2 * a) * x + 2 * x ^^^ 2 = 0" *)
1694 (*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"d2_polyeq_abcFormula_simplify"))*)
1695 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1696 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1697 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1698 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1699 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;introduc.MGs norm_Rational*)
1700 if f = Form' (FormKF (~1,EdUndef,0,Nundef,
1701 "[x = (-2 * a + 4 * b + sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4,\n x =\n (-2 * a + 4 * b + -1 * sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4]")) then writeln "simplify MG"
1702 else raise error "rlang.sml: diff.behav. in II 62b [x=...]";
1703 val asms = get_assumptions_ pt p;
1704 if asms = [(str2term"0 <= ((-2 * a + 4 * b + sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4 + a) ^^^ 2 + ((-2 * a + 4 * b + sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4 - 2 * b) ^^^ 2", []),
1705 (str2term"0 <= a + 2 * b", []),
1706 (str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) ^^^ 2", []),
1707 (str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) ^^^ 2", []),
1708 (str2term"0 <= ((-2 * a + 4 * b + -1 * sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4 + a) ^^^ 2 + ((-2 * a + 4 * b + -1 * sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4 - 2 * b) ^^^ 2", []),
1709 (str2term"0 <= a + 2 * b", []),
1710 (str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) ^^^ 2", []),
1711 (str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) ^^^ 2", [])]
1712 then writeln "should be simplified MG"
1713 else raise error "rlang.sml: diff.behav. in II 62b asms";
1715 "------ WN.TEST---------------------------------";
1716 "------ WN.TEST---------------------------------";
1717 "------ WN.TEST---------------------------------";
1719 val fmz = ["equality ((2*x+1)*x^^^2 = 0)",
1720 "solveFor x","solutions L"];
1721 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1722 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1723 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1724 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1725 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1726 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1727 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1729 val f = Form' (FormKF (~1,EdUndef,1,Nundef,"(2 * x + 1) * x ^^^ 2 = 0"))
1730 normiert nicht ... korr.WN:
1731 val t = str2term "(2*x+1)*x^^^2 = 0";
1732 val subst = [(str2term "bdv", str2term "x")];
1733 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
1734 if term2str t' = "x ^^^ 2 + 2 * x ^^^ 3 = 0" then ()
1735 else raise error "rlang.sml: 7";
1737 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1738 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1739 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1740 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1741 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1743 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1744 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1745 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1746 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1747 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1748 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = 0, x = -1 / 2]")) then()
1749 else raise error "rlang.sml WN.TEST new behaviour";
1751 "------ rlang.sml end---------------------------------";
1753 (*------------------------------vvv-Rewrite_Set "rat_eliminate"---------
1754 > trace_rewrite:=true;
1756 "(3 + -1 * x + 1 * x ^^^ 2) / (9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3) = 1 / x";
1757 > val SOME (t',asm) =
1758 rewrite_ thy dummy_ord rateq_erls true rat_mult_denominator_both t;
1759 > term2str t'; terms2str asm;
1760 "(3 + -1 * x + 1 * x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3)"
1761 "[\"9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3 ~= 0\",\"x ~= 0\"]"
1762 > trace_rewrite:=false;
1763 ------------------------------^^^-Rewrite_Set "rat_eliminate"---------*)
1766 "-------------------- WN.15.5.03: Pythagoras -------------------------------";
1767 "-------------------- WN.15.5.03: Pythagoras -------------------------------";
1768 "-------------------- WN.15.5.03: Pythagoras -------------------------------";
1770 val fmz = ["equality ((a/2)^^^2 + (b/2)^^^2 = r^^^2)",
1771 "solveFor a","solutions L"];
1772 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1773 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1774 (* Model_Problem ["normalize","polynomial","univariate","equation"])*)
1775 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1776 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1777 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1778 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1779 (*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalize_poly"])*)
1780 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1781 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1782 (*val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])*)
1783 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1784 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1785 (*val nxt =Model_Problem ["sq_only","degree_2","polynomial","univariate","equation"])*)
1786 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1787 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1788 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1789 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1790 (*val nxt = Apply_Method ["PolyEq","solve_d2_polyeq_sqonly_equation"])*)
1791 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1792 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1793 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1794 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1795 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1796 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1797 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1798 if f = Form' (FormKF (~1,EdUndef,0,Nundef,
1799 "[a = sqrt ((-1 * b ^^^ 2 + 4 * r ^^^ 2) / 1),\n a = -1 * sqrt ((-1 * b ^^^ 2 + 4 * r ^^^ 2) / 1)]")) andalso nxt = ("End_Proof'",End_Proof')
1800 then writeln"simplify result\nsimplify result\nsimplify result"
1801 else raise error "rlang.sml: diff.behav. in Pythagoras";
1802 val asms = get_assumptions_ pt p;
1803 (*if asms = [(str2term"0 <= -4 * (b ^^^ 2 / 4 + -4 * r ^^^ 2 / 4)", []),
1804 (str2term"0 <= -4 * (b ^^^ 2 / 4 + -4 * r ^^^ 2 / 4)", [])]*)
1806 "[(0 <= -4 * (b ^^^ 2 / 4 + -1 * r ^^^ 2 / 1), []),\
1807 \(0 <= -4 * (b ^^^ 2 / 4 + -1 * r ^^^ 2 / 1), [])]"
1808 then writeln"simplify result\nsimplify result\nsimplify result"
1809 else raise error "rlang.sml: diff.behav. in Pythagoras asms";
1812 "-------------------- WN.15.5.03: equation within the maximum example ------";
1813 "-------------------- WN.15.5.03: equation within the maximum example ------";
1814 "-------------------- WN.15.5.03: equation within the maximum example ------";
1816 val fmz = ["equality (2*sqrt(r^^^2 - (u/2)^^^2) - u^^^2/(2*sqrt(r^^^2 - (u/2)^^^2))= 0)",
1817 "solveFor u","solutions L"];
1818 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1820 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1821 (* Model_Problem ["normalize","root","univariate","equation"])*)
1822 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1823 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1824 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1825 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1826 (*val nxt = Apply_Method ["RootEq","norm_sq_root_equation"]) *)
1827 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1828 (*val nxt = Subproblem ("RootEq.thy",["univariate","equation"]))*)
1829 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1830 (*val nxt = Model_Problem ["sq","root","univariate","equation"]) *)
1831 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1832 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1833 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1834 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1835 (*val nxt = Apply_Method ["RootEq","solve_sq_root_equation"]) *)
1836 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1837 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1838 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1839 (*val nxt = Subproblem ("RootEq.thy",["univariate","equation"]))*)
1840 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1841 (*val nxt = Model_Problem ["rational","univariate","equation"]) *)
1842 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1843 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1844 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1845 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1846 (*val nxt = Apply_Method ["RootEq","solve_rat_equation"]) *)
1847 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1848 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1849 (*val nxt = Subproblem ("RootEq.thy",["univariate","equation"]))*)
1850 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1851 (*val nxt = Model_Problem ["normalize","polynomial","univariate","equation"]) *)
1852 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1853 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1854 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1855 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1856 (*val nxt = Apply_Method ["PolyEq","normalize_poly"]) *)
1857 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1858 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1859 (*val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
1866 "-16 * r ^^^ 4 + 8 * r ^^^ 2 * u ^^^ 2 = 0")) then ()
1867 else raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 38b";
1868 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1869 (*val nxt = Model_Problem ["sq_only","degree_2","polynomial","univariate","equation"]) *)
1870 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1871 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1872 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1873 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1874 (*val nxt = Apply_Method ["PolyEq","solve_d2_polyeq_sqonly_equation"]) *)
1875 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1876 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1877 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1878 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1879 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1880 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1881 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1882 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[u = sqrt (2 * r ^^^ 2 / 1), u = -1 * sqrt (2 * r ^^^ 2 / 1)]")) then()
1883 else raise error "rlang.sml WN.TEST new behaviour in max-rooteq";