|
1 (* use"../systest/details.sml"; |
|
2 use"systest/details.sml"; |
|
3 use"details.sml"; |
|
4 |
|
5 ######################################################## |
|
6 is NOT dependent on Test, but on other thys: |
|
7 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
8 uses from Rational.ML: Rrls cancel_p, Rrls cancel |
|
9 which in turn |
|
10 uses from Poly.ML: Rls make_polynomial, Rls expand_binom |
|
11 ######################################################## |
|
12 *) |
|
13 "-------- cancel, without detail ------------------------------"; |
|
14 "-------- cancel, detail rev-rew (cancel) afterwards ----------"; |
|
15 "-------------- cancel_p, without detail ------------------------------"; |
|
16 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------"; |
|
17 |
|
18 store_pbt |
|
19 (prep_pbt Test.thy |
|
20 (["test"], |
|
21 [], |
|
22 e_rls, None, [])); |
|
23 store_pbt |
|
24 (prep_pbt Test.thy |
|
25 (["detail","test"], |
|
26 [("#Given" ,["realTestGiven t_"]), |
|
27 ("#Find" ,["realTestFind s_"]) |
|
28 ], |
|
29 e_rls, None, [("Test.thy","test_detail")])); |
|
30 |
|
31 methods:= overwritel (!methods, |
|
32 [ |
|
33 prep_met |
|
34 (("Test.thy","test_detail_binom"):metID, |
|
35 [("#Given" ,["realTestGiven t_"]), |
|
36 ("#Find" ,["realTestFind s_"]) |
|
37 ], |
|
38 {rew_ord'="sqrt_right",rls'=tval_rls,calc = [],srls=e_rls,prls=e_rls, |
|
39 asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]}, |
|
40 "Script Testterm (g_::real) = \ |
|
41 \(((Rewrite_Set expand_binoms False) @@\ |
|
42 \ (Rewrite_Set cancel False)) g_)" |
|
43 ), |
|
44 prep_met |
|
45 (("Test.thy","test_detail_poly"):metID, |
|
46 [("#Given" ,["realTestGiven t_"]), |
|
47 ("#Find" ,["realTestFind s_"]) |
|
48 ], |
|
49 {rew_ord'="sqrt_right",rls'=tval_rls,calc=[],srls=e_rls,prls=e_rls, |
|
50 asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]}, |
|
51 "Script Testterm (g_::real) = \ |
|
52 \(((Rewrite_Set make_polynomial False) @@\ |
|
53 \ (Rewrite_Set cancel_p False)) g_)" |
|
54 )]); |
|
55 |
|
56 (*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*) |
|
57 |
|
58 "-------- cancel, without detail ------------------------------"; |
|
59 "-------- cancel, without detail ------------------------------"; |
|
60 "-------- cancel, without detail ------------------------------"; |
|
61 val fmz = ["realTestGiven (((3 + x) * (3 - x)) / ((3 + x) * (3 + x)))", |
|
62 "realTestFind s"]; |
|
63 val (dI',pI',mI') = |
|
64 ("Test.thy",["detail","test"],("Test.thy","test_detail_binom")); |
|
65 |
|
66 val p = e_pos'; val c = []; |
|
67 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
|
68 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; |
|
69 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
70 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
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 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*) |
|
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 (*"(3 + -1 * x) / (3 + x)"*) |
|
80 if nxt = ("End_Proof'",End_Proof') then () |
|
81 else raise error "details.sml, changed behaviour in: without detail"; |
|
82 |
|
83 |
|
84 "-------- cancel, detail rev-rew (cancel) afterwards ----------"; |
|
85 "-------- cancel, detail rev-rew (cancel) afterwards ----------"; |
|
86 "-------- cancel, detail rev-rew (cancel) afterwards ----------"; |
|
87 val p = e_pos'; val c = []; |
|
88 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
|
89 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; |
|
90 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
91 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
92 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
93 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
94 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
95 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*) |
|
96 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
97 (*val nxt = ("Rewrite_Set",Rewrite_Set "expand_binoms")*) |
|
98 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*) |
|
99 val nxt = ("Detail",Detail);"----------------------"; |
|
100 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
101 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
102 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
103 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
104 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
105 (*val nxt = ("End_Detail",End_Detail)*) |
|
106 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
107 (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel")*) |
|
108 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*) |
|
109 val nxt = ("Detail",Detail);"----------------------"; |
|
110 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e; |
|
111 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
112 (*15.10.02*) |
|
113 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
114 (* |
|
115 rewrite "Rationals.thy" "tless_true""e_rls"true("sym_real_plus_minus_binom","") |
|
116 "3 ^^^ 2 - x ^^^ 2"; |
|
117 *) |
|
118 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
119 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
120 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
121 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e; |
|
122 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
123 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 - x) / (3 + x)")) |
|
124 andalso nxt = ("End_Proof'",End_Proof') then () |
|
125 else raise error "new behaviour in details.sml, \ |
|
126 \cancel, rev-rew (cancel) afterwards"; |
|
127 |
|
128 (*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*) |
|
129 |
|
130 "-------------- cancel_p, without detail ------------------------------"; |
|
131 "-------------- cancel_p, without detail ------------------------------"; |
|
132 "-------------- cancel_p, without detail ------------------------------"; |
|
133 val fmz = ["realTestGiven (((3 + x)*(3+(-1)*x)) / ((3+x) * (3+x)))", |
|
134 "realTestFind s"]; |
|
135 val (dI',pI',mI') = |
|
136 ("Test.thy",["detail","test"],("Test.thy","test_detail_poly")); |
|
137 |
|
138 val p = e_pos'; val c = []; |
|
139 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
|
140 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; |
|
141 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
142 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
143 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
144 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
145 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
146 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*) |
|
147 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
148 "(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))"; |
|
149 |
|
150 (*14.3.03*) |
|
151 val t = str2term "(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))"; |
|
152 val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
|
153 "(9 + - (x ^^^ 2)) / (9 + 6 * x + x ^^^ 2)"; |
|
154 val Some (t,_) = rewrite_set_ thy false cancel_p t; term2str t; |
|
155 cancel_p_ thy t; |
|
156 |
|
157 val t = str2term "(3 + x) * (3 + -1 * x)"; |
|
158 val Some (t,_) = rewrite_set_ thy false expand_poly t; term2str t; |
|
159 "3 * 3 + 3 * (-1 * x) + (x * 3 + x * (-1 * x))"; |
|
160 val Some (t,_) = rewrite_set_ thy false order_add_mult t; term2str t; |
|
161 "3 * 3 + (3 * x + (-1 * (3 * x) + -1 * (x * x)))"; |
|
162 val Some (t,_) = rewrite_set_ thy false simplify_power t; term2str t; |
|
163 "3 ^^^ 2 + (3 * x + (-1 * (3 * x) + -1 * x ^^^ 2))"; |
|
164 val Some (t,_) = rewrite_set_ thy false collect_numerals t; term2str t; |
|
165 "9 + (0 * x + -1 * x ^^^ 2)"; |
|
166 val Some (t,_) = rewrite_set_ thy false reduce_012 t; term2str t; |
|
167 "9 + - (x ^^^ 2)"; |
|
168 (*14.3.03*) |
|
169 |
|
170 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
171 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
172 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
173 (*"(3 + -1 * x) / (3 + x)"*) |
|
174 if nxt = ("End_Proof'",End_Proof') then () |
|
175 else raise error "details.sml, changed behaviour in: cancel_p, without detail"; |
|
176 |
|
177 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------"; |
|
178 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------"; |
|
179 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------"; |
|
180 val p = e_pos'; val c = []; |
|
181 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
|
182 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; |
|
183 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
184 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
185 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
186 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
187 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
188 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*) |
|
189 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
190 (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*) |
|
191 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*) |
|
192 |
|
193 (*14.3.03.FIXXXXXME since Isa02/reverse-rew.sml: |
|
194 fun make_deriv ... Rls_ not yet impl. (| Thm | Calc) |
|
195 Rls_ needed for make_polynomial ---------------------- |
|
196 val nxt = ("Detail",Detail);"----------------------"; |
|
197 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
198 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
199 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
200 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
201 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
202 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
203 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
204 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
205 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
206 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
207 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
208 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
209 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
210 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
211 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
212 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
213 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
214 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
215 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
216 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
217 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
218 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
219 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
220 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
221 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
222 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
223 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
224 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
225 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
226 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
227 if nxt = ("End_Detail",End_Detail) then () |
|
228 else raise error "details.sml: new behav. in Detail make_polynomial"; |
|
229 ----------------------------------------------------------------------*) |
|
230 |
|
231 (*--------------- |
|
232 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
233 (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel_p")*) |
|
234 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*) |
|
235 val nxt = ("Detail",Detail);"----------------------"; |
|
236 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e; |
|
237 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
238 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
239 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
240 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
241 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
242 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e; |
|
243 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
244 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 + x) / (3 - x)")) |
|
245 andalso nxt = ("End_Proof'",End_Proof') then () |
|
246 else raise error "new behaviour in details.sml, cancel_p afterwards"; |
|
247 |
|
248 ----------------*) |
|
249 |
|
250 |
|
251 |
|
252 |
|
253 |
|
254 val fmz = ["realTestGiven ((x+3)+(-1)*(2+6*x))", |
|
255 "realTestFind s"]; |
|
256 val (dI',pI',mI') = |
|
257 ("Test.thy",["detail","test"],("Test.thy","test_detail_poly")); |
|
258 |
|
259 val p = e_pos'; val c = []; |
|
260 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
|
261 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; |
|
262 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
263 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
264 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
265 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
266 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
267 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*) |
|
268 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
269 (*16.10.02 --- kommt auf POLY_EXCEPTION ?!??? ---------------------------- |
|
270 (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*) |
|
271 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*) |
|
272 val nxt = ("Detail",Detail);"----------------------"; |
|
273 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
274 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
275 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
276 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
277 -------------------------------------------------------------------------*) |
|
278 |
|
279 |
|
280 |