1 (*8.01: aufgehoben wegen alter preconds, postconds*)
3 (* rectangle with maximal area, inscribed in a circle of fixed radius
5 problem-types and methods solving the respective problem-type
7 (1) names of the problem-types and methods and their hierarchy
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.
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
24 find-values find-values
26 (2) specification of the problem-types
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)) \
39 relate=["max_relation r","additionalRels RS"]};
40 (* ^^^ is exponenation *)
42 (* the functions Ex_frees, Rhs provide for the instantiation below *)
44 (* (1) instantiation of maximum, + variant in "values_for" *)
45 {given = ["fixed_values (R = #7)"],
46 where_= ["is_equality (R = #7)",
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 \
52 relate=["max_relation (A = a*b)",
53 "additionalRels [(a//#2)^^^#2 +(b//#2)^^^#2 =R^^^#2]"]};
54 (* R,a,b are bound by given, find *)
56 (* (2) instantiation of maximum *)
57 {given = ["fixed_values (R = #7)"],
58 where_= ["is_equality (R = #7)",
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 \
65 relate=["max_relation (A = a*b)",
66 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]};
67 (* R,A are bound by given, find *)
73 {given = ["equality (lhs = rhs)","bound_variable v","equalities es"],
75 find = ["function_term lhs_"],
78 (*the _ in lhs is used to transfer the lhs-identifier of equality*)
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]"],
84 find = ["function_term A_"(*=(a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))*)],
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]"],
92 find = ["function_term A_"(*=(#2*R*sin alpha *#2*R*cos alpha)*)],
97 (* max-of-fun-on-interval *)
98 (* ---------------------- *)
100 {given = ["function_term t","bound_variable v",
101 "domain {x::real. lower_bound <= x & x <= upper_bound}"],
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 *)
110 (* (1) variant of instantiation *)
111 {given = ["function_term (a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))",
113 "domain {x::real. #0 <= x & x <= #2*R}"],
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)"],
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}"],
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)"],
136 {given = ["function_term t","bound_variable bdv"],
138 find = ["derivative t'"],
139 with_ = ["t' is_derivative_of (%bdv. t)"],
141 (*the ' in t' is used to transfer the identifier from function_term*)
144 (* ["equation","univariate"] *)
145 (* ------------------------- *)
147 {given = ["equality (lhs = rhs)",
148 "bound_variable v","error_bound eps"],
150 find = ["solutions S"],
151 with_ = ["ALL s. s : S --> || (%v. lhs) s - (%v. rhs) s || <= eps"],
158 {given = ["max_relation r","additionalRels RS"],
160 find = ["values_for VS"],
164 (* (1) variant of instantiation *)
165 {given = ["max_relation (A = a*b)",
166 "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]"],
168 find = ["values_for [a,b]"],
172 (* (2) variant of instantiation *)
173 {given = ["max_relation (A = a*b)",],
175 find = ["values_for [A]",
176 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
181 (3) data-transfer between the the hidden formalization,
182 the root-problem and the sub-problems;
184 maximum -> #given.make-fun
186 maximum.#relate "max_relation r" -> "equality (lhs = rhs)"
187 formalization "bound_variable v" -> "bound_variable v"
188 maximum.#relate "additionalRels RS"-> "equalities es"
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. ...}"
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"
204 max-of-fun-on-interval + derivative ->
205 #given.["equation","univariate"]
206 ----------------------------------------------------------------
207 derivative.#find "derivative t'" -> "equality (lhs = rhs)"
209 make-fun.#given "bound_variable v" -> "bound_variable v"
210 formalization -> "error_bound eps"
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 "additionalRels RS"-> "additionalRels RS"
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 *)
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)) \
238 relate=["max_relation r","additionalRels rs"]}:string ppc;
239 val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
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}",
247 "max_relation A=#2*a*b - a^^^#2",
248 "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
249 "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
250 "additionalRels [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 \
258 relate=["max_relation (A=#2*a*b - a^^^#2)",
259 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
261 val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
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"],
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) \
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;
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"],
286 find=["function_term t"],with_=[(*???*)],
287 relate=[(*???*)]}: string ppc;
288 val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
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]"],
293 find=["function_term t"],
294 with_=[],relate=[]}: string ppc;
295 val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
297 "met --- make_explicit_and_substitute ---";
298 val met = {given=["equality e","bound_variable v", "equalities es"],
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"],
306 find=["function_term t"],with_=[(*???*)],
307 relate=[(*???*)]}: string ppc;
308 val chkmet = ((map (the o (parse thy))) o ppc2list) met;
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}"],
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;
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;
329 (* pbltyp --- max_of_fun --- *)
331 {given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;
332 val (SOME ct) = parse thy ;
333 atomty thy (Thm.term_of ct);
343 (* --- 14.1.00 --- *)
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;
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;
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;
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;
366 {given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;
367 val (SOME ct) = parse thy ;
368 atomty thy (Thm.term_of ct);