139 |
139 |
140 (* pbltyp --- max_of_fun --- *) |
140 (* pbltyp --- max_of_fun --- *) |
141 (* |
141 (* |
142 {given=[],where_=[],find=[],with_=[],relate=[]}: string ppc; |
142 {given=[],where_=[],find=[],with_=[],relate=[]}: string ppc; |
143 val (SOME ct) = parse thy ; |
143 val (SOME ct) = parse thy ; |
144 atomty (term_of ct); |
144 atomty (Thm.term_of ct); |
145 *) |
145 *) |
146 |
146 |
147 |
147 |
148 (* --- 14.1.00 ev. nicht ganz up to date bzg. oberem --- *) |
148 (* --- 14.1.00 ev. nicht ganz up to date bzg. oberem --- *) |
149 "p.114"; |
149 "p.114"; |
209 val formals = map (the o (parse thy)) ["A=#2*a*b - a^^^#2", |
209 val formals = map (the o (parse thy)) ["A=#2*a*b - a^^^#2", |
210 "a::real","{x. #0<x & x<R//#2}", |
210 "a::real","{x. #0<x & x<R//#2}", |
211 "{(a//#2)^^^#2 + (b//#2)^^^#2 = (R//#2)^^^#2}", |
211 "{(a//#2)^^^#2 + (b//#2)^^^#2 = (R//#2)^^^#2}", |
212 "{R::real}"]; |
212 "{R::real}"]; |
213 val tag__forms = chktyps thy (formals, givens); |
213 val tag__forms = chktyps thy (formals, givens); |
214 map ((atomty) o term_of) tag__forms; |
214 map ((atomty) o Thm.term_of) tag__forms; |
215 |
215 |
216 val formals = map (the o (parse thy)) ["A=#2*a*b - a^^^#2", |
216 val formals = map (the o (parse thy)) ["A=#2*a*b - a^^^#2", |
217 "alpha::real","{alpha. #0<alpha & alpha<pi//#2}", |
217 "alpha::real","{alpha. #0<alpha & alpha<pi//#2}", |
218 "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}", |
218 "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}", |
219 "{R::real}"]; |
219 "{R::real}"]; |
220 val tag__forms = chktyps thy (formals, givens); |
220 val tag__forms = chktyps thy (formals, givens); |
221 map ((atomty) o term_of) tag__forms; |
221 map ((atomty) o Thm.term_of) tag__forms; |
222 *) |
222 *) |
223 |
223 |
224 " --- subproblem: make-function-by-subst --- "; |
224 " --- subproblem: make-function-by-subst --- "; |
225 val origin = ["A=#2*a*b - a^^^#2", |
225 val origin = ["A=#2*a*b - a^^^#2", |
226 "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}", |
226 "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}", |
234 val with_ = ["||| Vars t ||| = #1"]; |
234 val with_ = ["||| Vars t ||| = #1"]; |
235 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_); |
235 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_); |
236 val givens = map (the o (parse thy)) given; |
236 val givens = map (the o (parse thy)) given; |
237 (* 5.3.00 |
237 (* 5.3.00 |
238 val tag__forms = chktyps thy (formals, givens); |
238 val tag__forms = chktyps thy (formals, givens); |
239 map ((atomty) o term_of) tag__forms; |
239 map ((atomty) o Thm.term_of) tag__forms; |
240 *) |
240 *) |
241 " --- subproblem: max-of-function --- "; |
241 " --- subproblem: max-of-function --- "; |
242 val origin = ["A = #2*(#2*R*(sin alpha))*(#2*R*(sin alpha)) - \ |
242 val origin = ["A = #2*(#2*R*(sin alpha))*(#2*R*(sin alpha)) - \ |
243 \ (#2*R*(sin alpha))^^^#2", |
243 \ (#2*R*(sin alpha))^^^#2", |
244 "{alpha. #0<alpha & alpha<pi//#2}", |
244 "{alpha. #0<alpha & alpha<pi//#2}", |
253 val with_ = ["||| Vars t ||| = #1"]; |
253 val with_ = ["||| Vars t ||| = #1"]; |
254 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_); |
254 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_); |
255 val givens = map (the o (parse thy)) given; |
255 val givens = map (the o (parse thy)) given; |
256 (* 5.3.00 |
256 (* 5.3.00 |
257 val tag__forms = chktyps thy (formals, givens); |
257 val tag__forms = chktyps thy (formals, givens); |
258 map ((atomty) o term_of) tag__forms; |
258 map ((atomty) o Thm.term_of) tag__forms; |
259 *) |
259 *) |
260 " --- subproblem: derivative --- "; |
260 " --- subproblem: derivative --- "; |
261 val origin = ["x^^^#3-y^^^#3+#-3*x+#12*y+#10","x::real"]; |
261 val origin = ["x^^^#3-y^^^#3+#-3*x+#12*y+#10","x::real"]; |
262 val formals = map (the o (parse thy)) origin; |
262 val formals = map (the o (parse thy)) origin; |
263 |
263 |
268 val with_ = ["t' is_derivative_of (%bdv. t)"]; |
268 val with_ = ["t' is_derivative_of (%bdv. t)"]; |
269 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_); |
269 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_); |
270 val givens = map (the o (parse thy)) given; |
270 val givens = map (the o (parse thy)) given; |
271 (* |
271 (* |
272 val tag__forms = chktyps thy (formals, givens); |
272 val tag__forms = chktyps thy (formals, givens); |
273 map ((atomty) o term_of) tag__forms; |
273 map ((atomty) o Thm.term_of) tag__forms; |
274 *) |
274 *) |
275 " --- subproblem: tan-quadrat-equation --- "; |
275 " --- subproblem: tan-quadrat-equation --- "; |
276 val origin = ["#8*R^^^#2*(cos alpha)^^^#2 + #-8*R^^^#2* \ |
276 val origin = ["#8*R^^^#2*(cos alpha)^^^#2 + #-8*R^^^#2* \ |
277 \ (cos alpha)*(sin alpha) + #8*R^^^#2*(sin alpha)^^^#2 = #0", |
277 \ (cos alpha)*(sin alpha) + #8*R^^^#2*(sin alpha)^^^#2 = #0", |
278 "alpha::real","#1//#1000"]; |
278 "alpha::real","#1//#1000"]; |
287 \ c*(sin bdv)) x || < epsilon}"]; |
287 \ c*(sin bdv)) x || < epsilon}"]; |
288 (* 5.3.00 |
288 (* 5.3.00 |
289 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_); |
289 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_); |
290 val givens = map (the o (parse thy)) given; |
290 val givens = map (the o (parse thy)) given; |
291 val tag__forms = chktyps thy (formals, givens); |
291 val tag__forms = chktyps thy (formals, givens); |
292 map ((atomty) o term_of) tag__forms; |
292 map ((atomty) o Thm.term_of) tag__forms; |
293 *) |
293 *) |
294 (* use"test-coil-kernel.sml"; |
294 (* use"test-coil-kernel.sml"; |
295 *) |
295 *) |
296 |
296 |
297 |
297 |