|
1 (* Title: Knowledge/polyeq-1.sml |
|
2 testexamples for PolyEq, poynomial equations and equational systems |
|
3 Author: Richard Lang 2003 |
|
4 (c) due to copyright terms |
|
5 WN030609: some expls dont work due to unfinished handling of 'expanded terms'; |
|
6 others marked with TODO have to be checked, too. |
|
7 *) |
|
8 |
|
9 "-----------------------------------------------------------------"; |
|
10 "table of contents -----------------------------------------------"; |
|
11 "-----------------------------------------------------------------"; |
|
12 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)"; |
|
13 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)"; |
|
14 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; |
|
15 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5"; |
|
16 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37"; |
|
17 "----------- rls make_polynomial_in ------------------------------"; |
|
18 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------"; |
|
19 "----------- rls d2_polyeq_bdv_only_simplify ---------------------"; |
|
20 "-----------------------------------------------------------------"; |
|
21 "-----------------------------------------------------------------"; |
|
22 |
|
23 |
|
24 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)"; |
|
25 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)"; |
|
26 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)"; |
|
27 val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)", |
|
28 "solveFor x","solutions L"]; |
|
29 val (dI',pI',mI') = |
|
30 ("PolyEq",["degree_2","expanded","univariate","equation"], |
|
31 ["PolyEq","complete_square"]); |
|
32 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
33 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
34 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
35 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
36 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
37 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
38 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
39 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
40 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
41 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
42 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
43 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
44 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
45 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
46 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
47 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
48 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
49 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
50 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f; |
|
51 (*WN.2.5.03 TODO FIXME Matthias ? |
|
52 case f of |
|
53 Form' |
|
54 (FormKF |
|
55 (~1,EdUndef,0,Nundef, |
|
56 "[x = (a + b) / 2 + -1 * sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b),\n x = (a + b) / 2 + sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b)]")) |
|
57 => () |
|
58 | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x^^^2 = 0"; |
|
59 this will be simplified [x = a, x = b] to by Factor.ML*) |
|
60 |
|
61 |
|
62 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)"; |
|
63 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)"; |
|
64 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)"; |
|
65 val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*) |
|
66 "solveFor x","solutions L"]; |
|
67 val (dI',pI',mI') = |
|
68 ("PolyEq",["degree_2","expanded","univariate","equation"], |
|
69 ["PolyEq","complete_square"]); |
|
70 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
71 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
72 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
73 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
74 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
75 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
76 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
77 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
78 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
79 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
80 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
81 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
82 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
83 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f; |
|
84 (*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]" |
|
85 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => () |
|
86 | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]"; |
|
87 *) |
|
88 |
|
89 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; |
|
90 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; |
|
91 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; |
|
92 val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*) |
|
93 "solveFor x","solutions L"]; |
|
94 val (dI',pI',mI') = |
|
95 ("PolyEq",["degree_2","expanded","univariate","equation"], |
|
96 ["PolyEq","complete_square"]); |
|
97 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
98 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
99 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
100 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
101 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
102 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
103 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
104 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
105 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
106 (*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" |
|
107 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => () |
|
108 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]"; |
|
109 *) |
|
110 if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then () |
|
111 else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]"; |
|
112 |
|
113 |
|
114 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5"; |
|
115 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5"; |
|
116 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5"; |
|
117 (*EP-17 Schalk_I_p86_n5*) |
|
118 val fmz = ["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"]; |
|
119 (* refine fmz ["univariate","equation"]; |
|
120 *) |
|
121 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); |
|
122 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
123 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
124 (* val nxt = |
|
125 ("Model_Problem", |
|
126 Model_Problem ["normalise","polynomial","univariate","equation"]) |
|
127 : string * tac*) |
|
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 nxt = |
|
134 ("Subproblem", |
|
135 Subproblem ("PolyEq",["polynomial","univariate","equation"])) |
|
136 : string * tac *) |
|
137 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
138 (*val nxt = |
|
139 ("Model_Problem", |
|
140 Model_Problem ["degree_1","polynomial","univariate","equation"]) |
|
141 : string * tac *) |
|
142 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
143 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
144 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
145 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
146 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
147 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
148 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
149 case f of FormKF "[x = 2]" => () |
|
150 | _ => error "polyeq.sml: diff.behav. in [x = 2]"; |
|
151 |
|
152 |
|
153 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37"; |
|
154 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37"; |
|
155 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37"; |
|
156 (*is in rlang.sml, too*) |
|
157 val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))", |
|
158 "solveFor x","solutions L"]; |
|
159 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); |
|
160 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
161 (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*) |
|
162 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
163 (* val nxt = |
|
164 ("Model_Problem", |
|
165 Model_Problem ["normalise","polynomial","univariate","equation"]) |
|
166 : string * tac *) |
|
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
172 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
173 (* val nxt = |
|
174 ("Subproblem", |
|
175 Subproblem ("PolyEq",["polynomial","univariate","equation"])) |
|
176 : string * tac*) |
|
177 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
178 (*val nxt = |
|
179 ("Model_Problem", |
|
180 Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"]) |
|
181 : string * tac*) |
|
182 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
183 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
184 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
185 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
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 case f of FormKF "[x = 2 / 15, x = 1]" => () |
|
190 | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]"; |
|
191 |
|
192 |
|
193 " -4 + x^^^2 =0 "; |
|
194 " -4 + x^^^2 =0 "; |
|
195 " -4 + x^^^2 =0 "; |
|
196 val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"]; |
|
197 (* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*) |
|
198 (*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*) |
|
199 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); |
|
200 (*val p = e_pos'; |
|
201 val c = []; |
|
202 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
|
203 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*) |
|
204 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
205 |
|
206 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
207 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
208 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
209 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
210 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
211 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
212 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
213 case f of FormKF "[x = 2, x = -2]" => () |
|
214 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -2]"; |
|
215 |
|
216 "----------- rls make_polynomial_in ------------------------------"; |
|
217 "----------- rls make_polynomial_in ------------------------------"; |
|
218 "----------- rls make_polynomial_in ------------------------------"; |
|
219 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*) |
|
220 (*WN.19.3.03 ---v-*) |
|
221 (*3(b)*)val (bdv,v) = (str2term "''bdv''", str2term "R1"); |
|
222 val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0"; |
|
223 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t; |
|
224 if term2str t' = "-1 * R * R2 + R2 * R1 + -1 * R * R1 = 0" then () |
|
225 else error "make_polynomial_in (-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0)"; |
|
226 "-1 * R * R2 + (R2 + -1 * R) * R1 = 0"; |
|
227 (*WN.19.3.03 ---^-*) |
|
228 |
|
229 (*3(c)*)val (bdv,v) = (str2term "bdv", str2term "p"); |
|
230 val t = str2term "y ^^^ 2 + -2 * (x * p) = 0"; |
|
231 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t; |
|
232 if term2str t' = "y ^^^ 2 + -2 * x * p = 0" then () |
|
233 else error "make_polynomial_in (y ^^^ 2 + -2 * (x * p) = 0)"; |
|
234 |
|
235 (*3(d)*)val (bdv,v) = (str2term "''bdv''", str2term "x2"); |
|
236 val t = str2term |
|
237 "A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1 * (x1 * (y2 * (1 / 2))) + -1 * (x3 * (y1 * (1 / 2 ))) + y1 * (1 / 2 * x2) + -1 * (y3 * (1 / 2 * x2)) = 0"; |
|
238 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t; |
|
239 if term2str t' = |
|
240 "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + -1 * x1 * y2 * (1 / 2) +\n-1 * x3 * y1 * (1 / 2) +\ny1 * (1 / 2) * x2 +\n-1 * y3 * (1 / 2) * x2 =\n0" |
|
241 then () |
|
242 else error "make_polynomial_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1..."; |
|
243 "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - x1 * y2 * (1 / 2) + - x3 * y1 * (1 / 2) + (y1 * (1 / 2) + - y3 * (1 / 2)) * x2 = 0"; |
|
244 |
|
245 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t; |
|
246 if term2str t' = |
|
247 "A / 1 + x1 * y3 / 2 + x3 * y2 / 2 + -1 * x1 * y2 / 2 + -1 * x3 * y1 / 2 +\ny1 * x2 / 2 +\n-1 * y3 * x2 / 2 =\n0" |
|
248 then () |
|
249 else error "make_ratpoly_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1..."; |
|
250 "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + -1 * x1 * y2 * (1 / 2) + -1 * x3 * y1 * (1 / 2) + (y1 * (1 / 2) + -1 * y3 * (1 / 2)) * x2 = 0"; |
|
251 |
|
252 (*3(e)*)val (bdv,v) = (str2term "bdv", str2term "a"); |
|
253 val t = str2term |
|
254 "A ^^^ 2 + c ^^^ 2 * (c / d) ^^^ 2 + (-4 * (c / d) ^^^ 2) * a ^^^ 2 = 0"; |
|
255 val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t; |
|
256 (* the invisible parentheses are as expected *) |
|
257 |
|
258 val t = str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0"; |
|
259 trace_rewrite:=(*true*)false; |
|
260 rewrite_set_ thy false expand_binoms t; |
|
261 trace_rewrite:=false; |
|
262 |
|
263 |
|
264 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------"; |
|
265 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------"; |
|
266 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------"; |
|
267 reset_states (); |
|
268 CalcTree |
|
269 [(["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"], |
|
270 ("PolyEq",["univariate","equation"],["no_met"]))]; |
|
271 Iterator 1; |
|
272 moveActiveRoot 1; |
|
273 |
|
274 autoCalculate 1 CompleteCalc; |
|
275 val ((pt,p),_) = get_calc 1; show_pt pt; |
|
276 interSteps 1 ([1],Res) |
|
277 (*BEFORE Isabelle2002 --> 2011: <ERROR> no Rewrite_Set... </ERROR> ?see fun prep_rls?*); |
|
278 |
|
279 |
|
280 "----------- rls d2_polyeq_bdv_only_simplify ---------------------"; |
|
281 "----------- rls d2_polyeq_bdv_only_simplify ---------------------"; |
|
282 "----------- rls d2_polyeq_bdv_only_simplify ---------------------"; |
|
283 val t = str2term "-6 * x + 5 * x ^^^ 2 = (0::real)"; |
|
284 val subst = [(str2term "(bdv::real)", str2term "(x::real)")]; |
|
285 val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t; |
|
286 (* steps in rls d2_polyeq_bdv_only_simplify:*) |
|
287 |
|
288 (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1","")) --> x * (-6 + 5 * x) = 0*) |
|
289 t |> term2str; t |> atomty; |
|
290 val thm = num_str @{thm d2_prescind1}; |
|
291 thm |> Thm.prop_of |> term2str; thm |> Thm.prop_of |> atomty; |
|
292 val SOME (t', _) = rewrite_inst_ thy e_rew_ord e_rls true subst thm t; term2str t'; |
|
293 |
|
294 (*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1","")) |
|
295 --> x = 0 | -6 + 5 * x = 0*) |
|
296 t' |> term2str; t' |> atomty; |
|
297 val thm = num_str @{thm d2_reduce_equation1}; |
|
298 thm |> Thm.prop_of |> term2str; thm |> Thm.prop_of |> atomty; |
|
299 val SOME (t'', _) = rewrite_inst_ thy e_rew_ord e_rls true subst thm t'; term2str t''; |
|
300 (* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))" |
|
301 instead d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))" |
|
302 *) |
|
303 if term2str t'' = "x = 0 \<or> -6 + 5 * x = 0" then () |
|
304 else error "rls d2_polyeq_bdv_only_simplify broken"; |