1 (* use"test-coil-kernel.sml"; |
|
2 W.N.22.11.99 |
|
3 |
|
4 *) |
|
5 |
|
6 (* vvv--- geht nicht wegen fun-types |
|
7 parse thy "case maxmin of is_max => (m' <= m) | is_min => (m <= m')"; |
|
8 parse thy "if maxmin = is_max then (m' <= m) else (m <= m')"; |
|
9 parse thy "if a=b then a else b"; |
|
10 parse thy "maxmin = is_max"; |
|
11 parse thy "maxmin =!= is_max"; |
|
12 ^^^--- geht nicht wegen fun-types *) |
|
13 |
|
14 "pbltyp --- maximum ---"; |
|
15 val pbltyp = {given=["fixedValues (cs::bool list)"], |
|
16 where_=[(*"foldl (op &) True (map is_equality cs)", |
|
17 "foldl (op &) True (map (Not o ((op <=) #0) o Rhs) cs)"*)], |
|
18 find=["maximum m","values_for (ms::real list)"], |
|
19 with_=[(*"Ex_frees ((foldl (op &) True (r#rs)) & \ |
|
20 \ (ALL m'. (subst (m,m') (foldl (op &) True (r#rs)) \ |
|
21 \ --> m' <= m)))"*)], |
|
22 relate=["max_relation r","additionalRels rs"]}:string ppc; |
|
23 val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp; |
|
24 "coil"; |
|
25 val org = ["fixedValues [R=(R::real)]", |
|
26 "boundVariable a","boundVariable b","boundVariable alpha", |
|
27 "domain {x::real. #0 <= x & x <= #2*R}", |
|
28 "domain {x::real. #0 <= x & x <= #2*R}", |
|
29 "domain {x::real. #0 <= x & x <= pi}", |
|
30 "errorBound (eps = #1//#1000)", |
|
31 "maximum A", |
|
32 (*"max_relation A=#2*a*b - a^^^#2",*) |
|
33 "relations [A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]", |
|
34 "relations [A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]", |
|
35 "relations [A=#2*a*b - a^^^#2, a=#2*R*sin alpha, b=#2*R*cos alpha]"]; |
|
36 val chkorg = map (the o (parse thy)) org; |
|
37 val pbl = {given=["fixedValues [R=(R::real)]"],where_=[], |
|
38 find=["maximum A","values_for [a,b]"], |
|
39 with_=[(* incompat.w. parse, ok with parseold |
|
40 "EX alpha. A=#2*a*b - a^^^#2 & \ |
|
41 \ a=#2*R*sin alpha & b=#2*R*cos alpha & \ |
|
42 \ (ALL A'. A'=#2*a*b - a^^^#2 & a=#2*R*sin alpha \ |
|
43 \ & b=#2*R*cos alpha \ |
|
44 \ --> A' <= A)"*)], |
|
45 relate=["relations [A=#2*a*b - a^^^#2, a=#2*R*sin alpha, b=#2*R*cos alpha]"] |
|
46 }: string ppc; |
|
47 val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl; |
|
48 |
|
49 "met --- maximum_by_differentiation ---"; |
|
50 val met = {given=["fixedValues (cs::bool list)","boundVariable v", |
|
51 "domain {x::real. lower_bound <= x & x<=upper_bound}", |
|
52 "errorBound epsilon"], |
|
53 where_=[], |
|
54 find=["maximum m","valuesFor (ms::bool list)", |
|
55 "function_term t","max_argument mx"], |
|
56 with_=[(* incompat.w. parse, ok with parseold |
|
57 "Ex_frees ((foldl (op &) True (mr#ars)) & \ |
|
58 \ (ALL m'. (subst (m,m') (foldl (op &) True (mr#ars))\ |
|
59 \ --> m' <= m))) & \ |
|
60 \m = (%v. t) mx & \ |
|
61 \( ALL x. lower_bound <= x & x <= upper_bound \ |
|
62 \ --> (%v. t) x <= m)"*)], |
|
63 relate=["max_relation mr", |
|
64 "additionalRels ars"]}: string ppc; |
|
65 val chkpbl = ((map (the o (parse thy))) o ppc2list) met; |
|
66 |
|
67 "data --- maximum_by_differentiation ---"; |
|
68 val met = {given=["fixedValues [R=(R::real)]","boundVariable alpha", |
|
69 "domain {x::real. #0 <= x & x <= pi//#2}", |
|
70 "errorBound (eps = #1//#1000)"], |
|
71 where_=[], |
|
72 find=["maximum A","valuesFor [a=Undef]", |
|
73 "function_term t","max_argument mx"], |
|
74 with_=[(* incompat.w. parse, ok with parseold |
|
75 "EX b alpha. A = #2*a*b - a^^^#2 & \ |
|
76 \ a = #2*R*sin alpha & \ |
|
77 \ b = #2*R*cos alpha & \ |
|
78 \ (ALL A'. A'= #2*a*b - a^^^#2 & \ |
|
79 \ a = #2*R*sin alpha & \ |
|
80 \ b = #2*R*cos alpha --> A' <= A) & \ |
|
81 \ A = (%alpha. t) mx & \ |
|
82 \ (ALL x. #0 <= x & x <= pi --> \ |
|
83 \ (%alpha. t) x <= A)"*)], |
|
84 relate=["max_relation mr", |
|
85 "additionalRels ars"]}: string ppc; |
|
86 val chkpbl = ((map (the o (parse thy))) o ppc2list) met; |
|
87 |
|
88 val (SOME ct) = parseold thy "EX b. (EX alpha. A = #2*a*b - a^^^#2)"; |
|
89 |
|
90 "pbltyp --- make_fun ---"; |
|
91 (* subproblem [(hd #relate root, equality), |
|
92 (boundVariable formalization, boundVariable), |
|
93 (tl #relate root, equalities)] *) |
|
94 val pbltyp = {given=["equality e","boundVariable v", "equalities es"], |
|
95 where_=[], |
|
96 find=["functionTerm t"],with_=[(*???*)], |
|
97 relate=[(*???*)]}: string ppc; |
|
98 val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp; |
|
99 "coil"; |
|
100 val pbl = {given=["equality (A=#2*a*b - a^^^#2)","boundVariable alpha", |
|
101 "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"], |
|
102 where_=[], |
|
103 find=["functionTerm t"], |
|
104 with_=[],relate=[]}: string ppc; |
|
105 val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl; |
|
106 |
|
107 "met --- make_explicit_and_substitute ---"; |
|
108 val met = {given=["equality e","boundVariable v", "equalities es"], |
|
109 where_=[], |
|
110 find=["functionTerm t"],with_=[(*???*)], |
|
111 relate=[(*???*)]}: string ppc; |
|
112 val chkmet = ((map (the o (parse thy))) o ppc2list) met; |
|
113 "met --- introduce_a_new_variable ---"; |
|
114 val met = {given=["equality e","boundVariable v", "substitutions es"], |
|
115 where_=[], |
|
116 find=["functionTerm t"],with_=[(*???*)], |
|
117 relate=[(*???*)]}: string ppc; |
|
118 val chkmet = ((map (the o (parse thy))) o ppc2list) met; |
|
119 |
|
120 |
|
121 "pbltyp --- max_of_fun_on_interval ---"; |
|
122 val pbltyp = {given=["functionTerm t","boundVariable v", |
|
123 "domain {x::real. lower_bound <= x & x <= upper_bound}"], |
|
124 where_=[], |
|
125 find=["maximums ms"], |
|
126 with_=[(* incompat.w. parse, ok with parseold |
|
127 "ALL m. m : ms --> \ |
|
128 \ (ALL x::real. lower_bound <= x & x <= upper_bound \ |
|
129 \ --> (%v. t) x <= m)"*)], |
|
130 relate=[]}: string ppc; |
|
131 val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp; |
|
132 "coil"; |
|
133 val pbl = {given=["functionTerm (f = #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \ |
|
134 \ (#2*R*sin alpha)^^^#2)","boundVariable alpha", |
|
135 "domain {x::real. #0 <= x & x <= pi}"],where_=[], |
|
136 find=["maximums [#1234]"],with_=[],relate=[]}: string ppc; |
|
137 val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl; |
|
138 |
|
139 |
|
140 (* pbltyp --- max_of_fun --- *) |
|
141 (* |
|
142 {given=[],where_=[],find=[],with_=[],relate=[]}: string ppc; |
|
143 val (SOME ct) = parse thy ; |
|
144 atomty (term_of ct); |
|
145 *) |
|
146 |
|
147 |
|
148 (* --- 14.1.00 ev. nicht ganz up to date bzg. oberem --- *) |
|
149 "p.114"; |
|
150 val org = {given=["[u=(#12::real)]"],where_=[], |
|
151 find=["[a,(b::real)]"],with_=[], |
|
152 relate=["[is_max A=a*(b::real), #2*a+#2*b=(u::real)]"]}: string ppc; |
|
153 val chkorg = ((map (the o (parse thy))) o ppc2list) org; |
|
154 "p.116"; |
|
155 val org = {given=["[c=#10, h=(#4::real)]"],where_=[], |
|
156 find=["[x,(y::real)]"],with_=[], |
|
157 relate=["[A=x*(y::real), c//h=x//(h-(y::real))]"]}: string ppc; |
|
158 val chkorg = ((map (the o (parse thy))) o ppc2list) org; |
|
159 "p.117"; |
|
160 val org = {given=["[r=#5]"],where_=[], |
|
161 find=["[x,(y::real)]"],with_=[], |
|
162 relate=["[is_max #0=pi*x^^^#2 + pi*x*(r::real)]"]}: string ppc; |
|
163 val chkorg = ((map (the o (parse thy))) o ppc2list) org; |
|
164 "#241"; |
|
165 val org = {given=["[s=(#10::real)]"],where_=[], |
|
166 find=["[p::real]"],with_=[], |
|
167 relate=["[is_max p=n*m, s=n+(m::real)]"]}: string ppc; |
|
168 val chkorg = ((map (the o (parse thy))) o ppc2list) org; |
|
169 |
|
170 |
|
171 |
|
172 (* -------------- coil-kernel -------------- vor 19.1.00 *) |
|
173 (* --- subproblem: make-function-by-subst ~~~~~~~~~~~ *) |
|
174 (* --- subproblem: max-of-function *) |
|
175 (* --- subproblem: derivative *) |
|
176 (* --- subproblem: tan-quadrat-equation *) |
|
177 "-------------- coil-kernel --------------"; |
|
178 val origin = ["A=#2*a*b - a^^^#2", |
|
179 "a::real","b::real","{x. #0<x & x<R//#2}", |
|
180 "{(a//#2)^^^#2 + (b//#2)^^^#2 = (R//#2)^^^#2}", |
|
181 "alpha::real","{alpha::real. #0<alpha & alpha<pi//#2}", |
|
182 "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}", |
|
183 "{R::real}"]; |
|
184 (* --- for a isa-users-mail --- FIXME |
|
185 Goal "{x. x < a} = ?z"; |
|
186 {x::'a. x < a} = ?z |
|
187 Goal "{x. x < #3} = {a}"; |
|
188 {x::'a. x < (#3::'a)} = {a} |
|
189 Goal "{x. #3 < x} = ?z"; |
|
190 Collect (op < (#3::'a)) = ?z |
|
191 ---------------------------- *) |
|
192 |
|
193 val formals = map (the o (parse thy)) origin; |
|
194 |
|
195 val given = ["formula_for_max (lhs=rhs)","boundVariable bdv", |
|
196 "interval {x. low < x & x < high}", |
|
197 "additional_conds ac","constants cs"]; |
|
198 val where_ = ["lhs is_const","bdv is_const","low is_const","high is_const", |
|
199 "||| Vars equ ||| = ||| VarsSet ac ||| - ||| ac ||| + #1"]; |
|
200 val find = ["f::real => real","maxs::real set"]; |
|
201 val with_ = [(* incompat.w. parse, ok with parseold |
|
202 "maxs = {m. low < m & m < high & \ |
|
203 \ (m is_local_max_of (%bdv. f))}"*)]; |
|
204 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_); |
|
205 val givens = map (the o (parse thy)) given; |
|
206 |
|
207 "------- 1.1 -------"; |
|
208 (* 5.3.00 |
|
209 val formals = map (the o (parse thy)) ["A=#2*a*b - a^^^#2", |
|
210 "a::real","{x. #0<x & x<R//#2}", |
|
211 "{(a//#2)^^^#2 + (b//#2)^^^#2 = (R//#2)^^^#2}", |
|
212 "{R::real}"]; |
|
213 val tag__forms = chktyps thy (formals, givens); |
|
214 map ((atomty) o term_of) tag__forms; |
|
215 |
|
216 val formals = map (the o (parse thy)) ["A=#2*a*b - a^^^#2", |
|
217 "alpha::real","{alpha. #0<alpha & alpha<pi//#2}", |
|
218 "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}", |
|
219 "{R::real}"]; |
|
220 val tag__forms = chktyps thy (formals, givens); |
|
221 map ((atomty) o term_of) tag__forms; |
|
222 *) |
|
223 |
|
224 " --- subproblem: make-function-by-subst --- "; |
|
225 val origin = ["A=#2*a*b - a^^^#2", |
|
226 "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}", |
|
227 "{R::real}"]; |
|
228 val formals = map (the o (parse thy)) origin; |
|
229 |
|
230 val given = ["equation (lhs=rhs)","substitutions ss", |
|
231 "constants cs"]; |
|
232 val where_ = []; |
|
233 val find = ["t::real"]; |
|
234 val with_ = ["||| Vars t ||| = #1"]; |
|
235 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_); |
|
236 val givens = map (the o (parse thy)) given; |
|
237 (* 5.3.00 |
|
238 val tag__forms = chktyps thy (formals, givens); |
|
239 map ((atomty) o term_of) tag__forms; |
|
240 *) |
|
241 " --- subproblem: max-of-function --- "; |
|
242 val origin = ["A = #2*(#2*R*(sin alpha))*(#2*R*(sin alpha)) - \ |
|
243 \ (#2*R*(sin alpha))^^^#2", |
|
244 "{alpha. #0<alpha & alpha<pi//#2}", |
|
245 "{R::real}"]; |
|
246 val formals = map (the o (parse thy)) origin; |
|
247 |
|
248 val given = ["equation (lhs=rhs)", |
|
249 "interval {x. low < x & x < high}", |
|
250 "constants cs"]; |
|
251 val where_ = ["lhs is_const","low is_const","high is_const"]; |
|
252 val find = ["t::real"]; |
|
253 val with_ = ["||| Vars t ||| = #1"]; |
|
254 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_); |
|
255 val givens = map (the o (parse thy)) given; |
|
256 (* 5.3.00 |
|
257 val tag__forms = chktyps thy (formals, givens); |
|
258 map ((atomty) o term_of) tag__forms; |
|
259 *) |
|
260 " --- subproblem: derivative --- "; |
|
261 val origin = ["x^^^#3-y^^^#3+#-3*x+#12*y+#10","x::real"]; |
|
262 val formals = map (the o (parse thy)) origin; |
|
263 |
|
264 val given = ["functionTerm t", |
|
265 "boundVariable bdv"]; |
|
266 val where_ = ["bdv is_const"]; |
|
267 val find = ["t'::real"]; |
|
268 val with_ = ["t' is_derivative_of (%bdv. t)"]; |
|
269 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_); |
|
270 val givens = map (the o (parse thy)) given; |
|
271 (* |
|
272 val tag__forms = chktyps thy (formals, givens); |
|
273 map ((atomty) o term_of) tag__forms; |
|
274 *) |
|
275 " --- subproblem: tan-quadrat-equation --- "; |
|
276 val origin = ["#8*R^^^#2*(cos alpha)^^^#2 + #-8*R^^^#2* \ |
|
277 \ (cos alpha)*(sin alpha) + #8*R^^^#2*(sin alpha)^^^#2 = #0", |
|
278 "alpha::real","#1//#1000"]; |
|
279 val formals = map (the o (parse thy)) origin; |
|
280 |
|
281 val given = ["equation (a*(cos bdv)^^^#2 + b*(cos bdv)*(sin bdv) + \ |
|
282 \ c*(sin bdv) = #0)", |
|
283 "boundVariable bdv","errorBound epsilon"]; |
|
284 val where_ = ["bdv is_const","epsilon is_const_expr"]; |
|
285 val find = ["L::real set"]; |
|
286 val with_ = ["L = {x. || (%bdv. a*(cos bdv)^^^#2 + b*(cos bdv)*(sin bdv) + \ |
|
287 \ c*(sin bdv)) x || < epsilon}"]; |
|
288 (* 5.3.00 |
|
289 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_); |
|
290 val givens = map (the o (parse thy)) given; |
|
291 val tag__forms = chktyps thy (formals, givens); |
|
292 map ((atomty) o term_of) tag__forms; |
|
293 *) |
|
294 (* use"test-coil-kernel.sml"; |
|
295 *) |
|
296 |
|
297 |
|
298 " #################################################### "; |
|
299 " test specify "; |
|
300 " #################################################### "; |
|
301 |
|
302 |
|
303 val cts = |
|
304 ["fixedValues [R=(R::real)]", |
|
305 "boundVariable a", "boundVariable b", |
|
306 "boundVariable alpha", |
|
307 "domain {x::real. #0 <= x & x <= #2*R}", |
|
308 "domain {x::real. #0 <= x & x <= #2*R}", |
|
309 "domain {x::real. #0 <= x & x <= pi//#2}", |
|
310 "errorBound (eps = #1//#1000)", |
|
311 "maximum A","valuesFor [a=Undef]", |
|
312 (*"functionTerm t","max_argument mx", |
|
313 "max_relation (A=#2*a*b - a^^^#2)", *) |
|
314 "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", |
|
315 "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", |
|
316 "additionalRels [A=#2*a*b - a^^^#2,a=#2*R*sin alpha, b=#2*R*cos alpha]"]; |
|
317 val (dI',pI',mI')= |
|
318 ("DiffAppl.thy",["Script.thy","maximum_of","function"],e_metID); |
|
319 val c = []:cid; |
|
320 |
|
321 (* |
|
322 val pbl = {given=["fixedValues [R=(R::real)]","boundVariable alpha", |
|
323 "domain {x::real. #0 <= x & x <= pi//#2}", |
|
324 "errorBound (eps = #1//#1000)"], |
|
325 where_=[], |
|
326 find=["maximum A","valuesFor [a=Undef]"(*, |
|
327 "functionTerm t","max_argument mx"*)], |
|
328 with_=[], |
|
329 relate=["max_relation (A=#2*a*b - a^^^#2)", |
|
330 "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", |
|
331 "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", |
|
332 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"] |
|
333 }: string ppc; |
|
334 *) |
|
335 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = |
|
336 specify (Init_Proof (cts,(dI',pI',mI'))) e_pos' [] EmptyPtree; |
|
337 |
|
338 val ct = "fixedValues [R=(R::real)]"; |
|
339 (*l(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify(Add_Given ct) p c pt*) |
|
340 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt; |
|
341 |
|
342 val ct = "boundVariable a"; |
|
343 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt; |
|
344 val ct = "boundVariable alpha"; |
|
345 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt; |
|
346 |
|
347 val ct = "domain {x::real. #0 <= x & x <= pi//#2}"; |
|
348 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt; |
|
349 |
|
350 val ct = "errorBound (eps = (#1::real) // #1000)"; |
|
351 val ct = "maximum A"; |
|
352 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt; |
|
353 |
|
354 val ct = "valuesFor [a=Undef]"; |
|
355 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt; |
|
356 |
|
357 val ct = "max_relation ()"; |
|
358 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt; |
|
359 |
|
360 val ct = "relations [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]"; |
|
361 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt; |
|
362 |
|
363 (* ... nxt = Specify_Domain ... |
|
364 val ct = "additionalRels [b=#2*R*cos alpha]"; |
|
365 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = |
|
366 specify(Add_Relation ct) p c pt; |
|
367 (* |
|
368 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt; |
|
369 *) |
|
370 val ct = "additionalRels [a=#2*R*sin alpha]"; |
|
371 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = |
|
372 specify(Add_Relation ct) p c pt; |
|
373 (* |
|
374 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt; |
|
375 *) |
|
376 *) |
|
377 (* --- tricky case (termlist interleaving variants): |
|
378 > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = |
|
379 specify (Init_Proof (cts,(dI,pI,mI))) [] [] EmptyPtree; |
|
380 |
|
381 > val ct = "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2, b=#2*R*cos alpha]"; |
|
382 > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt; |
|
383 *) |
|
384 |
|
385 (* --- incomplete input --- |
|
386 > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = |
|
387 specify (Init_Proof (cts,(dI,pI,mI))) [] [] EmptyPtree; |
|
388 |
|
389 > val ct = "[R=(R::real)]"; |
|
390 > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt; |
|
391 |
|
392 > val ct = "R=(R::real)"; |
|
393 > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt; |
|
394 |
|
395 > val ct = "(R::real)"; |
|
396 > specify nxt p c pt; |
|
397 *) |
|
398 |
|
399 |
|
400 " #################################################### "; |
|
401 " test do_ specify "; |
|
402 " #################################################### "; |
|
403 |
|
404 |
|
405 val cts = ["fixedValues [R=(R::real)]", |
|
406 "boundVariable a", "boundVariable b", |
|
407 "boundVariable alpha", |
|
408 "domain {x::real. #0 <= x & x <= #2*R}", |
|
409 "domain {x::real. #0 <= x & x <= #2*R}", |
|
410 "domain {x::real. #0 <= x & x <= pi//#2}", |
|
411 "errorBound (eps=#1//#1000)", |
|
412 "maximum A","valuesFor [a=Undef]", |
|
413 (*"functionTerm t","max_argument mx", *) |
|
414 "max_relation (A=#2*a*b - a^^^#2)", |
|
415 "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", |
|
416 "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", |
|
417 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]; |
|
418 val (dI',pI',mI')= |
|
419 ("DiffAppl.thy",["DiffAppl.thy","test_maximum"],e_metID); |
|
420 val p = e_pos'; val c = []; |
|
421 |
|
422 val (mI,m) = ("Init_Proof",Init_Proof (cts, (dI',pI',mI'))); |
|
423 val (pst as (sc,pt,cl):pstate) = (EmptyScr, e_ptree, []); |
|
424 val (p,_,f,nxt,_,(_,pt,_)) = do_ (mI,m) p c pst; |
|
425 (*val nxt = ("Add_Given",Add_Given "fixedValues [R = R]")*) |
|
426 |
|
427 val (p,_,Form' (PpcKF (_,_,ppc)),nxt,_,(_,pt,_)) = |
|
428 do_ nxt p c (EmptyScr,pt,[]); |
|
429 (*val nxt = ("Add_Given",Add_Given "boundVariable a") *) |
|