|
1 (*8.01: aufgehoben wegen alter preconds, postconds*) |
|
2 |
|
3 (* rectangle with maximal area, inscribed in a circle of fixed radius |
|
4 |
|
5 problem-types and methods solving the respective problem-type |
|
6 |
|
7 (1) names of the problem-types and methods and their hierarchy |
|
8 as subproblems. |
|
9 names of problem-types are string lists (diss 5.3.), not shown |
|
10 here with exception of ["equation","univariate"] in order to |
|
11 indicate, that this particular problem needs refinement to a |
|
12 more specific type of equation solvable by tan-square, etc. |
|
13 |
|
14 problem-types methods |
|
15 ------------------------------- ---------------------- |
|
16 maximum maximum-by-differentiation |
|
17 maximum-by-experimentation |
|
18 make-fun make-explicit-and-substitute |
|
19 introduce-a-new-variable |
|
20 max-of-fun-on-interval max-of-fun-on-interval |
|
21 derivative differentiate |
|
22 ["equation","univariate"] tan-square |
|
23 |
|
24 find-values find-values |
|
25 |
|
26 (2) specification of the problem-types |
|
27 *) |
|
28 |
|
29 (* maximum *) |
|
30 (* ------- *) |
|
31 (* problem-type *) |
|
32 {given = ["fixed_values (cs::bool list)"], |
|
33 where_= ["foldl (op &) True (map is_equality cs)", |
|
34 "foldl (op &) True (map (Not o ((op <=) #0) o Rhs) cs)"], |
|
35 find=["maximum m","values_for (ms::real list)"], |
|
36 with_=["Ex_frees ((foldl (op &) True (r#RS)) & \ |
|
37 \ (ALL m'. (subst (m,m') (foldl (op &) True (r#RS)) \ |
|
38 \ --> m' <= m)))"], |
|
39 relate=["max_relation r","additional_relations RS"]}; |
|
40 (* ^^^ is exponenation *) |
|
41 |
|
42 (* the functions Ex_frees, Rhs provide for the instantiation below *) |
|
43 |
|
44 (* (1) instantiation of maximum, + variant in "values_for" *) |
|
45 {given = ["fixed_values (R = #7)"], |
|
46 where_= ["is_equality (R = #7)", |
|
47 "Not (R <= #0)"], |
|
48 find =["maximum A","values_for [a,b]"], |
|
49 with_ =["EX A. A = a*b & (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2 \ |
|
50 \ (ALL A'. A' = a*b & (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2 \ |
|
51 \ --> A' <= A)))"], |
|
52 relate=["max_relation (A = a*b)", |
|
53 "additional_relations [(a//#2)^^^#2 +(b//#2)^^^#2 =R^^^#2]"]}; |
|
54 (* R,a,b are bound by given, find *) |
|
55 |
|
56 (* (2) instantiation of maximum *) |
|
57 {given = ["fixed_values (R = #7)"], |
|
58 where_= ["is_equality (R = #7)", |
|
59 "Not (R <= #0)"], |
|
60 find =["maximum A","values_for [A]"], |
|
61 with_ =["EX a b alpha. A = a*b & \ |
|
62 \ a = #2*R*sin alpha & b =#2*R*cos alpha &\ |
|
63 \ (ALL A'. A' = a*b & a = #2*R*sin alpha & b =#2*R*cos alpha \ |
|
64 \ --> A' <= A)))"], |
|
65 relate=["max_relation (A = a*b)", |
|
66 "additional_relations [a=#2*R*sin alpha, b=#2*R*cos alpha]"]}; |
|
67 (* R,A are bound by given, find *) |
|
68 |
|
69 |
|
70 (* make-fun *) |
|
71 (* -------- *) |
|
72 (* problem-type *) |
|
73 {given = ["equality (lhs = rhs)","bound_variable v","equalities es"], |
|
74 where_= [], |
|
75 find = ["function_term lhs_"], |
|
76 with_ = [(*???*)], |
|
77 relate= [(*???*)]}; |
|
78 (*the _ in lhs is used to transfer the lhs-identifier of equality*) |
|
79 |
|
80 (* (1) instantiation for make-explicit-and-substitute *) |
|
81 {given = ["equality A = a * b","bound_variable a", |
|
82 "equalities [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"], |
|
83 where_= [], |
|
84 find = ["function_term A_"(*=(a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))*)], |
|
85 with_ = [], |
|
86 relate= []}; |
|
87 |
|
88 (* (2) instantiation for introduce-a-new-variable *) |
|
89 {given = ["equality A = a * b","bound_variable alpha", |
|
90 "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"], |
|
91 where_= [], |
|
92 find = ["function_term A_"(*=(#2*R*sin alpha *#2*R*cos alpha)*)], |
|
93 with_ = [], |
|
94 relate= []}; |
|
95 |
|
96 |
|
97 (* max-of-fun-on-interval *) |
|
98 (* ---------------------- *) |
|
99 (* problem-type *) |
|
100 {given = ["function_term t","bound_variable v", |
|
101 "domain {x::real. lower_bound <= x & x <= upper_bound}"], |
|
102 where_= [], |
|
103 find = ["maximums ms"], |
|
104 with_ = ["ALL m. m : ms --> \ |
|
105 \ (ALL x::real. lower_bound <= x & x <= upper_bound \ |
|
106 \ --> (%v. t) x <= m)"], |
|
107 relate= []}: string ppc; |
|
108 (* ':' is 'element', '::' is a type constraint *) |
|
109 |
|
110 (* (1) variant of instantiation *) |
|
111 {given = ["function_term (a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))", |
|
112 "bound_variable a", |
|
113 "domain {x::real. #0 <= x & x <= #2*R}"], |
|
114 where_= [], |
|
115 find = ["maximums AM"], |
|
116 with_ = ["ALL am. am : AM --> \ |
|
117 \ (ALL x::real. #0 <= x & x <= #2*R \ |
|
118 \ --> (%a. (a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))) x <= am)"], |
|
119 relate= []}; |
|
120 |
|
121 (* (2) variant of instantiation *) |
|
122 {given = ["function_term (#2*R*sin alpha * #2*R*cos alpha)", |
|
123 "bound_variable alpha", |
|
124 "domain {x::real. #0 <= x & x <= pi//#2}"], |
|
125 where_= [], |
|
126 find = ["maximums AM"], |
|
127 with_ = ["ALL am. am : AM --> \ |
|
128 \ (ALL x::real. #0 <= x & x <= pi//#2 \ |
|
129 \ --> (%alpha. (#2*R*sin alpha * #2*R*cos alpha)) x <= am)"], |
|
130 relate= []}; |
|
131 |
|
132 |
|
133 (* derivative *) |
|
134 (* ---------- *) |
|
135 (* problem-type *) |
|
136 {given = ["function_term t","bound_variable bdv"], |
|
137 where_= [], |
|
138 find = ["derivative t'"], |
|
139 with_ = ["t' is_derivative_of (%bdv. t)"], |
|
140 relate= []}; |
|
141 (*the ' in t' is used to transfer the identifier from function_term*) |
|
142 |
|
143 |
|
144 (* ["equation","univariate"] *) |
|
145 (* ------------------------- *) |
|
146 (* problem-type *) |
|
147 {given = ["equality (lhs = rhs)", |
|
148 "bound_variable v","error_bound eps"], |
|
149 where_= [], |
|
150 find = ["solutions S"], |
|
151 with_ = ["ALL s. s : S --> || (%v. lhs) s - (%v. rhs) s || <= eps"], |
|
152 relate= []}; |
|
153 |
|
154 |
|
155 (* find-values *) |
|
156 (* ----------- *) |
|
157 (* problem-type *) |
|
158 {given = ["max_relation r","additional_relations RS"], |
|
159 where_= [], |
|
160 find = ["values_for VS"], |
|
161 with_ = [(*???*)], |
|
162 relate= []}; |
|
163 |
|
164 (* (1) variant of instantiation *) |
|
165 {given = ["max_relation (A = a*b)", |
|
166 "additional_relations [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]"], |
|
167 where_= [], |
|
168 find = ["values_for [a,b]"], |
|
169 with_ = [], |
|
170 relate= []}; |
|
171 |
|
172 (* (2) variant of instantiation *) |
|
173 {given = ["max_relation (A = a*b)",], |
|
174 where_= [], |
|
175 find = ["values_for [A]", |
|
176 "additional_relations [a=#2*R*sin alpha, b=#2*R*cos alpha]"], |
|
177 with_ = [], |
|
178 relate= []}; |
|
179 |
|
180 (* |
|
181 (3) data-transfer between the the hidden formalization, |
|
182 the root-problem and the sub-problems; |
|
183 |
|
184 maximum -> #given.make-fun |
|
185 ------------------- |
|
186 maximum.#relate "max_relation r" -> "equality (lhs = rhs)" |
|
187 formalization "bound_variable v" -> "bound_variable v" |
|
188 maximum.#relate "additional_relations RS"-> "equalities es" |
|
189 |
|
190 |
|
191 maximum + make-fun -> #given.max-of-fun-on-interval |
|
192 -------------------------------------------- |
|
193 make-fun.#find "function_term lhs_" -> "function_term t" |
|
194 make-fun.#given "bound_variable v" -> "bound_variable v" |
|
195 formalization -> "domain {x::real. ...}" |
|
196 |
|
197 |
|
198 max-of-fun-on-interval -> #given.derivative |
|
199 ------------------------------------ |
|
200 make-fun.#find "function_term lhs_" -> "function_term t" |
|
201 make-fun.#given "bound_variable v" -> "bound_variable bdv" |
|
202 |
|
203 |
|
204 max-of-fun-on-interval + derivative -> |
|
205 #given.["equation","univariate"] |
|
206 ---------------------------------------------------------------- |
|
207 derivative.#find "derivative t'" -> "equality (lhs = rhs)" |
|
208 (* t'= #0 *) |
|
209 make-fun.#given "bound_variable v" -> "bound_variable v" |
|
210 formalization -> "error_bound eps" |
|
211 |
|
212 |
|
213 maximum + make-fun + max-of-fun-on-interval -> #given.find-values |
|
214 ---------------------------------------------------------- |
|
215 maximum.#relate "max_relation r" -> "max_relation r" |
|
216 maximum.#relate "additional_relations RS"-> "additional_relations RS" |
|
217 *) |
|
218 |
|
219 |
|
220 |
|
221 |
|
222 (* vvv--- geht nicht wegen fun-types |
|
223 parse thy "case maxmin of is_max => (m' <= m) | is_min => (m <= m')"; |
|
224 parse thy "if maxmin = is_max then (m' <= m) else (m <= m')"; |
|
225 parse thy "if a=b then a else b"; |
|
226 parse thy "maxmin = is_max"; |
|
227 parse thy "maxmin =!= is_max"; |
|
228 ^^^--- geht nicht wegen fun-types *) |
|
229 |
|
230 "pbltyp --- maximum ---"; |
|
231 val pbltyp = {given=["fixed_values (cs::bool list)"], |
|
232 where_=["foldl (op &) True (map is_equality cs)", |
|
233 "foldl (op &) True (map (Not o ((op <=) #0) o Rhs) cs)"], |
|
234 find=["maximum m","values_for (ms::real list)"], |
|
235 with_=["Ex_frees ((foldl (op &) True (r#rs)) & \ |
|
236 \ (ALL m'. (subst (m,m') (foldl (op &) True (r#rs)) \ |
|
237 \ --> m' <= m)))"], |
|
238 relate=["max_relation r","additional_relations rs"]}:string ppc; |
|
239 val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp; |
|
240 "coil"; |
|
241 val org = ["fixed_values [R=(R::real)]", |
|
242 "bound_variable a", "bound_variable b", "bound_variable alpha", |
|
243 "domain {x::real. #0 <= x & x <= #2*R}", |
|
244 "domain {x::real. #0 <= x & x <= #2*R}", |
|
245 "domain {x::real. #0 <= x & x <= pi}", |
|
246 "maximum A", |
|
247 "max_relation A=#2*a*b - a^^^#2", |
|
248 "additional_relations [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]", |
|
249 "additional_relations [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]", |
|
250 "additional_relations [a=#2*R*sin alpha, b=#2*R*cos alpha]"]; |
|
251 val chkorg = map (the o (parse thy)) org; |
|
252 val pbl = {given=["fixed_values [R=(R::real)]"],where_=[], |
|
253 find=["maximum A","values_for [a,b]"], |
|
254 with_=["EX alpha. A=#2*a*b - a^^^#2 & \ |
|
255 \ a=#2*R*sin alpha & b=#2*R*cos alpha & \ |
|
256 \ (ALL A'. A'=#2*a*b - a^^^#2 & a=#2*R*sin alpha & b=#2*R*cos alpha \ |
|
257 \ --> A' <= A)"], |
|
258 relate=["max_relation (A=#2*a*b - a^^^#2)", |
|
259 "additional_relations [a=#2*R*sin alpha, b=#2*R*cos alpha]"] |
|
260 }: string ppc; |
|
261 val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl; |
|
262 |
|
263 "met --- maximum_by_differentiation ---"; |
|
264 val met = {given=["fixed_values (cs::bool list)","bound_variable v", |
|
265 "domain {x::real. lower_bound <= x & x <= upper_bound}", |
|
266 "approximation apx"], |
|
267 where_=[], |
|
268 find=["maximum m","values_for (ms::real list)", |
|
269 "function_term t","max_argument mx"], |
|
270 with_=["Ex_frees ((foldl (op &) True (rs::bool list)) & \ |
|
271 \ (ALL m'. (subst (m,m') (foldl (op &) True rs) \ |
|
272 \ --> m' <= m))) & \ |
|
273 \m = (%v. t) mx & \ |
|
274 \( ALL x. lower_bound <= x & x <= upper_bound \ |
|
275 \ --> (%v. t) x <= m)"], |
|
276 relate=["rs::bool list"]}: string ppc; |
|
277 val chkpbl = ((map (the o (parse thy))) o ppc2list) met; |
|
278 |
|
279 |
|
280 "pbltyp --- make_fun ---"; |
|
281 (* subproblem [(hd #relate root, equality), |
|
282 (bound_variable formalization, bound_variable), |
|
283 (tl #relate root, equalities)] *) |
|
284 val pbltyp = {given=["equality e","bound_variable v", "equalities es"], |
|
285 where_=[], |
|
286 find=["function_term t"],with_=[(*???*)], |
|
287 relate=[(*???*)]}: string ppc; |
|
288 val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp; |
|
289 "coil"; |
|
290 val pbl = {given=["equality (A=#2*a*b - a^^^#2)","bound_variable alpha", |
|
291 "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"], |
|
292 where_=[], |
|
293 find=["function_term t"], |
|
294 with_=[],relate=[]}: string ppc; |
|
295 val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl; |
|
296 |
|
297 "met --- make_explicit_and_substitute ---"; |
|
298 val met = {given=["equality e","bound_variable v", "equalities es"], |
|
299 where_=[], |
|
300 find=["function_term t"],with_=[(*???*)], |
|
301 relate=[(*???*)]}: string ppc; |
|
302 val chkmet = ((map (the o (parse thy))) o ppc2list) met; |
|
303 "met --- introduce_a_new_variable ---"; |
|
304 val met = {given=["equality e","bound_variable v", "substitutions es"], |
|
305 where_=[], |
|
306 find=["function_term t"],with_=[(*???*)], |
|
307 relate=[(*???*)]}: string ppc; |
|
308 val chkmet = ((map (the o (parse thy))) o ppc2list) met; |
|
309 |
|
310 |
|
311 "pbltyp --- max_of_fun_on_interval ---"; |
|
312 val pbltyp = {given=["function_term t","bound_variable v", |
|
313 "domain {x::real. lower_bound <= x & x <= upper_bound}"], |
|
314 where_=[], |
|
315 find=["maximums ms"], |
|
316 with_=["ALL m. m : ms --> \ |
|
317 \ (ALL x::real. lower_bound <= x & x <= upper_bound \ |
|
318 \ --> (%v. t) x <= m)"], |
|
319 relate=[]}: string ppc; |
|
320 val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp; |
|
321 "coil"; |
|
322 val pbl = {given=["function_term #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \ |
|
323 \ (#2*R*sin alpha)^^^#2","bound_variable alpha", |
|
324 "domain {x::real. #0 <= x & x <= pi}"],where_=[], |
|
325 find=["maximums [#1234]"],with_=[],relate=[]}: string ppc; |
|
326 val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl; |
|
327 |
|
328 |
|
329 (* pbltyp --- max_of_fun --- *) |
|
330 (* |
|
331 {given=[],where_=[],find=[],with_=[],relate=[]}: string ppc; |
|
332 val (SOME ct) = parse thy ; |
|
333 atomty thy (term_of ct); |
|
334 *) |
|
335 |
|
336 |
|
337 |
|
338 |
|
339 |
|
340 |
|
341 |
|
342 |
|
343 (* --- 14.1.00 --- *) |
|
344 "p.114"; |
|
345 val org = {given=["[u=(#12::real)]"],where_=[], |
|
346 find=["[a,(b::real)]"],with_=[], |
|
347 relate=["[is_max A=a*(b::real), #2*a+#2*b=(u::real)]"]}: string ppc; |
|
348 val chkorg = ((map (the o (parse thy))) o ppc2list) org; |
|
349 "p.116"; |
|
350 val org = {given=["[c=#10, h=(#4::real)]"],where_=[], |
|
351 find=["[x,(y::real)]"],with_=[], |
|
352 relate=["[A=x*(y::real), c//h=x//(h-(y::real))]"]}: string ppc; |
|
353 val chkorg = ((map (the o (parse thy))) o ppc2list) org; |
|
354 "p.117"; |
|
355 val org = {given=["[r=#5]"],where_=[], |
|
356 find=["[x,(y::real)]"],with_=[], |
|
357 relate=["[is_max #0=pi*x^^^#2 + pi*x*(r::real)]"]}: string ppc; |
|
358 val chkorg = ((map (the o (parse thy))) o ppc2list) org; |
|
359 "#241"; |
|
360 val org = {given=["[s=(#10::real)]"],where_=[], |
|
361 find=["[p::real]"],with_=[], |
|
362 relate=["[is_max p=n*m, s=n+(m::real)]"]}: string ppc; |
|
363 val chkorg = ((map (the o (parse thy))) o ppc2list) org; |
|
364 |
|
365 (* |
|
366 {given=[],where_=[],find=[],with_=[],relate=[]}: string ppc; |
|
367 val (SOME ct) = parse thy ; |
|
368 atomty thy (term_of ct); |
|
369 *) |