|
1 (* use"../smltest/IsacKnowledge/rlang.sml"; |
|
2 use"rlang.sml"; |
|
3 *) |
|
4 |
|
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 *******************************************************************) |
|
11 |
|
12 |
|
13 |
|
14 (*WN.12.6.03: for TODOs search 'writeln', for simplification search MG*) |
|
15 (* use"kbtest/rlang.sml"; |
|
16 use"rlang.sml"; |
|
17 (c) Richard Lang 2003 |
|
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. |
|
21 created: 030228 |
|
22 by: rlang |
|
23 last change: 030603 |
|
24 *) |
|
25 (*@Book{bSchalk1, |
|
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}, |
|
31 year = {1986}, |
|
32 note = {Schulbuch-Nr. 942}, |
|
33 } |
|
34 |
|
35 @Book{bSchalk2, |
|
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}, |
|
42 year = {1987}, |
|
43 note = {Schulbuch-Nr. 1682}, |
|
44 } |
|
45 *) |
|
46 |
|
47 (* Compiler.Control.Print.printDepth:=5; (*4 default*) |
|
48 trace_rewrite:=true; |
|
49 trace_rewrite:=false; |
|
50 refine fmz ["univariate","equation"]; |
|
51 *) |
|
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)"; |
|
57 (*EP*) |
|
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"]); |
|
61 (*val p = e_pos'; |
|
62 val c = []; |
|
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; |
|
76 |
|
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]"; |
|
83 |
|
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)"; |
|
88 (*EP*) |
|
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"]); |
|
92 (*val p = e_pos'; |
|
93 val c = []; |
|
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]"; |
|
113 |
|
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))"; |
|
118 (*EP*) |
|
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"]); |
|
122 (*val p = e_pos'; |
|
123 val c = []; |
|
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]"; |
|
143 |
|
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)"; |
|
148 (*EP*) |
|
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"]); |
|
152 (*val p = e_pos'; |
|
153 val c = []; |
|
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]"; |
|
173 |
|
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))"; |
|
178 (*ER-2*) |
|
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 []"; |
|
201 |
|
202 (*WN---v *) |
|
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"; |
|
209 |
|
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"; |
|
214 (*WN---^ *) |
|
215 |
|
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)"; |
|
220 (*ER-1*) |
|
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"]); |
|
224 (*val p = e_pos'; |
|
225 val c = []; |
|
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]"; |
|
244 |
|
245 |
|
246 (*WN---v *) |
|
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; |
|
250 term2str t'; |
|
251 if term2str t' = "79 / 12 + 65 / 36 * x = 0" then () |
|
252 else raise error "rlang.sml: 3"; |
|
253 (*WN---^ *) |
|
254 |
|
255 |
|
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)"; |
|
260 (*ER-3*) |
|
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"]); |
|
264 (*val p = e_pos'; |
|
265 val c = []; |
|
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]"; |
|
295 |
|
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)"; |
|
300 (*ER-4*) |
|
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"]); |
|
304 (*val p = e_pos'; |
|
305 val c = []; |
|
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]"; |
|
336 |
|
337 |
|
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)"; |
|
342 (*ER-5*) |
|
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"]); |
|
346 (*val p = e_pos'; |
|
347 val c = []; |
|
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; |
|
352 *) |
|
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]"; |
|
369 |
|
370 (*WN---v *) |
|
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"; |
|
376 |
|
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"; |
|
382 (*WN---^ *) |
|
383 |
|
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)"; |
|
388 (*ER-6*) |
|
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]"; |
|
420 |
|
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)"; |
|
425 (*ER-7*) |
|
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*) |
|
486 |
|
487 (*22.10.03: |
|
488 val it = "9 * x + (x ^^^ 3 + -6 * x ^^^ 2) ~= 0" : string; |
|
489 before 22.10.03: |
|
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]"; |
|
506 |
|
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)"; |
|
511 (*ER-8*) |
|
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"]); |
|
515 |
|
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]"; |
|
546 |
|
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)"; |
|
551 (*ER-10*) |
|
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"]); |
|
555 |
|
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]"; |
|
575 |
|
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)"; |
|
580 (*ER-11*) |
|
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"]); |
|
584 |
|
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"]))*) |
|
609 if f = Form' |
|
610 (FormKF |
|
611 (~1, |
|
612 EdUndef, |
|
613 0, |
|
614 Nundef, |
|
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")*) |
|
639 |
|
640 get_assumptions_ pt p; |
|
641 (*it = ["v + w ~= 0"] ... goes to the solution as an assumption*) |
|
642 |
|
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"; |
|
653 |
|
654 |
|
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)"; |
|
659 (*ER-12*) |
|
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; |
|
678 if f = Form' |
|
679 (FormKF |
|
680 (~1, |
|
681 EdUndef, |
|
682 0, |
|
683 Nundef, |
|
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"; |
|
702 |
|
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)"; |
|
707 (*ER-9*) |
|
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; |
|
727 if f = Form' |
|
728 (FormKF |
|
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"; |
|
747 |
|
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"; |
|
779 |
|
780 |
|
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)"; |
|
785 (*EO ??*) |
|
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"]); |
|
789 (*val p = e_pos'; |
|
790 val c = []; |
|
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"; |
|
812 |
|
813 |
|
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)"; |
|
818 (*EO-8*) |
|
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"]); |
|
822 (*val p = e_pos'; |
|
823 val c = []; |
|
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; |
|
830 |
|
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; |
|
835 |
|
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); |
|
851 |
|
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"; |
|
863 |
|
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)))"; |
|
868 (*ER-14*) |
|
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"]); |
|
872 (*val p = e_pos'; |
|
873 val c = []; |
|
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"; |
|
895 |
|
896 (*-------------------- Schalk II ----------------------------*) |
|
897 (*-------------------- Schalk II ----------------------------*) |
|
898 (*-------------------- Schalk II ----------------------------*) |
|
899 (*-------------------- Schalk II ----------------------------*) |
|
900 (*-------------------- Schalk II ----------------------------*) |
|
901 |
|
902 |
|
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))"; |
|
907 (*EO*) |
|
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"]); |
|
911 (*val p = e_pos'; |
|
912 val c = []; |
|
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]"; |
|
941 |
|
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"]); |
|
949 (*val p = e_pos'; |
|
950 val c = []; |
|
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; |
|
983 if f = Form' |
|
984 (FormKF |
|
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; |
|
1006 if asms2str asms = |
|
1007 "[(0 <= (25 * (1 / 9) + -1 * (16 + 49 * (1 / 9))) * -56, []),\ |
|
1008 \(0 <= 1 / 9, []),\ |
|
1009 \(0 <= 1 / 9, []),\ |
|
1010 \(0 <= (-5 + 7 * sqrt (1 / 9) + 1) * 5, []),\ |
|
1011 \(0 <= 1 / 9, []),\ |
|
1012 \(0 <= (25 * (1 / 9) + -1 * (16 + 49 * (1 / 9))) * -56, []),\ |
|
1013 \(0 <= 1 / 9, [])]" |
|
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"; |
|
1023 |
|
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))"; |
|
1028 (*EO-2*) |
|
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"]); |
|
1032 |
|
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"; |
|
1073 |
|
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))"; |
|
1078 (*EO-3*) |
|
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"]); |
|
1082 |
|
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]"; |
|
1124 |
|
1125 |
|
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))"; |
|
1130 (*EO-4*) |
|
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"]); |
|
1134 |
|
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; |
|
1187 |
|
1188 |
|
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)"; |
|
1193 (*EP*) |
|
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"]); |
|
1197 (*val p = e_pos'; |
|
1198 val c = []; |
|
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 []"; |
|
1218 |
|
1219 |
|
1220 (*----------------- Schalk II s.66 Bsp 8a ------------------------*) |
|
1221 "Schalk II s.66 Bsp 8a ((x - 4)/(x+4) = (1 - x)/(1+x))"; |
|
1222 (*ER-15*) |
|
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"]); |
|
1226 |
|
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", ...])*) |
|
1247 (* |
|
1248 val Form' (FormKF (~1, EdUndef, 0, Nundef, str)) = f; |
|
1249 *) |
|
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]"; |
|
1261 |
|
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"]); |
|
1269 (*val p = e_pos'; |
|
1270 val c = []; |
|
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; |
|
1286 if f = Form' |
|
1287 (FormKF |
|
1288 (~1, |
|
1289 EdUndef, |
|
1290 0, |
|
1291 Nundef, |
|
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*) |
|
1301 |
|
1302 |
|
1303 (*----------------- Schalk II s.66 Bsp 20a ------------------------*) |
|
1304 (*EO-6*) |
|
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"]); |
|
1311 (*val p = e_pos'; |
|
1312 val c = []; |
|
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]"; |
|
1349 |
|
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" |
|
1356 ### or2list False |
|
1357 ([6, 6, 3, 1], Res) "False" |
|
1358 *) |
|
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"]); |
|
1362 |
|
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; |
|
1384 if f = Form' |
|
1385 (FormKF |
|
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 []"; |
|
1397 |
|
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"]); |
|
1405 (*val p = e_pos'; |
|
1406 val c = []; |
|
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; |
|
1421 (*if f = Form' |
|
1422 (FormKF |
|
1423 (~1, |
|
1424 EdUndef, |
|
1425 0, |
|
1426 Nundef, |
|
1427 "c ^^^ 4 / d ^^^ 2 + A ^^^ 2 * d ^^^ 2 / d ^^^ 2 +\n-4 * c ^^^ 2 / d ^^^ 2 * a ^^^ 2 =\n0")) then ()*) |
|
1428 if f2str f = |
|
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=...]"; |
|
1442 |
|
1443 |
|
1444 |
|
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; |
|
1459 (*val p = ([3],Res) |
|
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"]))*) |
|
1475 if f = Form' |
|
1476 (FormKF |
|
1477 (~1, |
|
1478 EdUndef, |
|
1479 0, |
|
1480 Nundef, |
|
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"; |
|
1506 |
|
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; |
|
1520 |
|
1521 ... with sml-nj: |
|
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 |
|
1527 *) |
|
1528 |
|
1529 (* |
|
1530 "(a + b * x) / (a + -1 * (b * x)) + -1 * (a + -1 * (b * x)) / (a + b * x) =\n4 * a * b / (a ^^^ 2 + -1 * b ^^^ 2)" |
|
1531 |
|
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)" |
|
1535 |
|
1536 |
|
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; |
|
1540 term2str t'; |
|
1541 trace_rewrite:=false; |
|
1542 |
|
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) |
|
1544 |
|
1545 ## rls: discard_minus on: |
|
1546 ## rls: powers on: |
|
1547 ## rls: rat_mult_divide on: |
|
1548 ## rls: expand 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) |
|
1553 |
|
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) |
|
1556 |
|
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) |
|
1559 |
|
1560 ### try calc: op *' |
|
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) |
|
1562 |
|
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 |
|
1566 |
|
1567 ## rls: discard_minus on: |
|
1568 ## rls: powers on: |
|
1569 ## rls: rat_mult_divide on: |
|
1570 ## rls: expand 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) |
|
1574 |
|
1575 ## rls: order_add_mult on: |
|
1576 |
|
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 |
|
1580 |
|
1581 ## rls: discard_minus on: |
|
1582 ## rls: powers on: |
|
1583 ## rls: rat_mult_divide on: |
|
1584 ## rls: expand 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 |
|
1591 *) |
|
1592 |
|
1593 |
|
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"]); |
|
1599 |
|
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; |
|
1624 if f = Form' |
|
1625 (FormKF |
|
1626 (~1, |
|
1627 EdUndef, |
|
1628 0, |
|
1629 Nundef, |
|
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 !!!*) |
|
1654 |
|
1655 |
|
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; |
|
1677 if f = Form' |
|
1678 (FormKF |
|
1679 (~1, |
|
1680 EdUndef, |
|
1681 0, |
|
1682 Nundef, |
|
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"; |
|
1714 |
|
1715 "------ WN.TEST---------------------------------"; |
|
1716 "------ WN.TEST---------------------------------"; |
|
1717 "------ WN.TEST---------------------------------"; |
|
1718 (*EO-7*) |
|
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; |
|
1728 (* |
|
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"; |
|
1736 *) |
|
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; |
|
1742 |
|
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"; |
|
1750 |
|
1751 "------ rlang.sml end---------------------------------"; |
|
1752 |
|
1753 (*------------------------------vvv-Rewrite_Set "rat_eliminate"--------- |
|
1754 > trace_rewrite:=true; |
|
1755 > val t = str2term |
|
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"---------*) |
|
1764 |
|
1765 |
|
1766 "-------------------- WN.15.5.03: Pythagoras -------------------------------"; |
|
1767 "-------------------- WN.15.5.03: Pythagoras -------------------------------"; |
|
1768 "-------------------- WN.15.5.03: Pythagoras -------------------------------"; |
|
1769 (*EO-9*) |
|
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)", [])]*) |
|
1805 if asms2str asms = |
|
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"; |
|
1810 |
|
1811 |
|
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 ------"; |
|
1815 (*EO-10*) |
|
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"]); |
|
1819 |
|
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"]))*) |
|
1860 if f = Form' |
|
1861 (FormKF |
|
1862 (~1, |
|
1863 EdUndef, |
|
1864 0, |
|
1865 Nundef, |
|
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"; |