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