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 (* \<up> 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) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2 \
50 \ (ALL A'. A' = a*b & (a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2 \
52 relate=["max_relation (A = a*b)",
53 "additionalRels [(a//#2) \<up> #2 +(b//#2) \<up> #2 =R \<up> #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) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2]"],
84 find = ["function_term A_"(*=(a * #2 * sqrt(R \<up> #2 - (a//#2) \<up> #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 model;
108 (* ':' is 'element', '::' is a type constraint *)
110 (* (1) variant of instantiation *)
111 {given = ["function_term (a * #2 * sqrt(R \<up> #2 - (a//#2) \<up> #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 \<up> #2 - (a//#2) \<up> #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) \<up> #2 + (b//#2) \<up> #2 =R \<up> #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 \<up> --- 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 model;
239 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) 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 \<up> #2",
248 "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2]",
249 "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #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 \<up> #2 & \
255 \ a=#2*R*sin alpha & b=#2*R*cos alpha & \
256 \ (ALL A'. A'=#2*a*b - a \<up> #2 & a=#2*R*sin alpha & b=#2*R*cos alpha \
258 relate=["max_relation (A=#2*a*b - a \<up> #2)",
259 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
261 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) 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 model;
277 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) 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 model;
288 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
290 val pbl = {given=["equality (A=#2*a*b - a \<up> #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 model;
295 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) 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 model;
302 val chkmet = ((map (the o (parse thy))) o P_Model.to_list) 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 model;
308 val chkmet = ((map (the o (parse thy))) o P_Model.to_list) 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 model;
320 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
322 val pbl = {given=["function_term #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \
323 \ (#2*R*sin alpha) \<up> #2", "bound_variable alpha",
324 "domain {x::real. #0 <= x & x <= pi}"],where_=[],
325 find=["maximums [#1234]"],with_=[],relate=[]}: string model;
326 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
329 (* pbltyp --- max_of_fun --- *)
331 {given=[],where_=[],find=[],with_=[],relate=[]}: string model;
332 val (SOME ct) = parse thy ;
333 TermC.atom_trace_detail @{context} (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 model;
348 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) 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 model;
353 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
355 val org = {given=["[r=#5]"],where_=[],
356 find=["[x,(y::real)]"],with_=[],
357 relate=["[is_max #0=pi*x \<up> #2 + pi*x*(r::real)]"]}: string model;
358 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) 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 model;
363 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
366 {given=[],where_=[],find=[],with_=[],relate=[]}: string model;
367 val (SOME ct) = parse thy ;
368 TermC.atom_trace_detail @{context} (Thm.term_of ct);