1.1 --- a/src/Tools/isac/IsacKnowledge/DiffApp-oldpbl.sml Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,369 +0,0 @@
1.4 -(*8.01: aufgehoben wegen alter preconds, postconds*)
1.5 -
1.6 -(* rectangle with maximal area, inscribed in a circle of fixed radius
1.7 -
1.8 -problem-types and methods solving the respective problem-type
1.9 -
1.10 -(1) names of the problem-types and methods and their hierarchy
1.11 - as subproblems.
1.12 - names of problem-types are string lists (diss 5.3.), not shown
1.13 - here with exception of ["equation","univariate"] in order to
1.14 - indicate, that this particular problem needs refinement to a
1.15 - more specific type of equation solvable by tan-square, etc.
1.16 -
1.17 -problem-types methods
1.18 -------------------------------- ----------------------
1.19 -maximum maximum-by-differentiation
1.20 - maximum-by-experimentation
1.21 - make-fun make-explicit-and-substitute
1.22 - introduce-a-new-variable
1.23 - max-of-fun-on-interval max-of-fun-on-interval
1.24 - derivative differentiate
1.25 - ["equation","univariate"] tan-square
1.26 -
1.27 - find-values find-values
1.28 -
1.29 -(2) specification of the problem-types
1.30 -*)
1.31 -
1.32 -(* maximum *)
1.33 -(* ------- *)
1.34 -(* problem-type *)
1.35 -{given = ["fixed_values (cs::bool list)"],
1.36 - where_= ["foldl (op &) True (map is_equality cs)",
1.37 - "foldl (op &) True (map (Not o ((op <=) #0) o Rhs) cs)"],
1.38 - find=["maximum m","values_for (ms::real list)"],
1.39 - with_=["Ex_frees ((foldl (op &) True (r#RS)) & \
1.40 - \ (ALL m'. (subst (m,m') (foldl (op &) True (r#RS)) \
1.41 - \ --> m' <= m)))"],
1.42 - relate=["max_relation r","additional_relations RS"]};
1.43 -(* ^^^ is exponenation *)
1.44 -
1.45 -(* the functions Ex_frees, Rhs provide for the instantiation below *)
1.46 -
1.47 -(* (1) instantiation of maximum, + variant in "values_for" *)
1.48 -{given = ["fixed_values (R = #7)"],
1.49 - where_= ["is_equality (R = #7)",
1.50 - "Not (R <= #0)"],
1.51 - find =["maximum A","values_for [a,b]"],
1.52 - with_ =["EX A. A = a*b & (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2 \
1.53 - \ (ALL A'. A' = a*b & (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2 \
1.54 - \ --> A' <= A)))"],
1.55 - relate=["max_relation (A = a*b)",
1.56 - "additional_relations [(a//#2)^^^#2 +(b//#2)^^^#2 =R^^^#2]"]};
1.57 -(* R,a,b are bound by given, find *)
1.58 -
1.59 -(* (2) instantiation of maximum *)
1.60 -{given = ["fixed_values (R = #7)"],
1.61 - where_= ["is_equality (R = #7)",
1.62 - "Not (R <= #0)"],
1.63 - find =["maximum A","values_for [A]"],
1.64 - with_ =["EX a b alpha. A = a*b & \
1.65 - \ a = #2*R*sin alpha & b =#2*R*cos alpha &\
1.66 - \ (ALL A'. A' = a*b & a = #2*R*sin alpha & b =#2*R*cos alpha \
1.67 - \ --> A' <= A)))"],
1.68 - relate=["max_relation (A = a*b)",
1.69 - "additional_relations [a=#2*R*sin alpha, b=#2*R*cos alpha]"]};
1.70 -(* R,A are bound by given, find *)
1.71 -
1.72 -
1.73 -(* make-fun *)
1.74 -(* -------- *)
1.75 -(* problem-type *)
1.76 -{given = ["equality (lhs = rhs)","bound_variable v","equalities es"],
1.77 - where_= [],
1.78 - find = ["function_term lhs_"],
1.79 - with_ = [(*???*)],
1.80 - relate= [(*???*)]};
1.81 -(*the _ in lhs is used to transfer the lhs-identifier of equality*)
1.82 -
1.83 -(* (1) instantiation for make-explicit-and-substitute *)
1.84 -{given = ["equality A = a * b","bound_variable a",
1.85 - "equalities [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"],
1.86 - where_= [],
1.87 - find = ["function_term A_"(*=(a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))*)],
1.88 - with_ = [],
1.89 - relate= []};
1.90 -
1.91 -(* (2) instantiation for introduce-a-new-variable *)
1.92 -{given = ["equality A = a * b","bound_variable alpha",
1.93 - "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
1.94 - where_= [],
1.95 - find = ["function_term A_"(*=(#2*R*sin alpha *#2*R*cos alpha)*)],
1.96 - with_ = [],
1.97 - relate= []};
1.98 -
1.99 -
1.100 -(* max-of-fun-on-interval *)
1.101 -(* ---------------------- *)
1.102 -(* problem-type *)
1.103 -{given = ["function_term t","bound_variable v",
1.104 - "domain {x::real. lower_bound <= x & x <= upper_bound}"],
1.105 - where_= [],
1.106 - find = ["maximums ms"],
1.107 - with_ = ["ALL m. m : ms --> \
1.108 - \ (ALL x::real. lower_bound <= x & x <= upper_bound \
1.109 - \ --> (%v. t) x <= m)"],
1.110 - relate= []}: string ppc;
1.111 -(* ':' is 'element', '::' is a type constraint *)
1.112 -
1.113 -(* (1) variant of instantiation *)
1.114 -{given = ["function_term (a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))",
1.115 - "bound_variable a",
1.116 - "domain {x::real. #0 <= x & x <= #2*R}"],
1.117 - where_= [],
1.118 - find = ["maximums AM"],
1.119 - with_ = ["ALL am. am : AM --> \
1.120 - \ (ALL x::real. #0 <= x & x <= #2*R \
1.121 - \ --> (%a. (a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))) x <= am)"],
1.122 - relate= []};
1.123 -
1.124 -(* (2) variant of instantiation *)
1.125 -{given = ["function_term (#2*R*sin alpha * #2*R*cos alpha)",
1.126 - "bound_variable alpha",
1.127 - "domain {x::real. #0 <= x & x <= pi//#2}"],
1.128 - where_= [],
1.129 - find = ["maximums AM"],
1.130 - with_ = ["ALL am. am : AM --> \
1.131 - \ (ALL x::real. #0 <= x & x <= pi//#2 \
1.132 - \ --> (%alpha. (#2*R*sin alpha * #2*R*cos alpha)) x <= am)"],
1.133 - relate= []};
1.134 -
1.135 -
1.136 -(* derivative *)
1.137 -(* ---------- *)
1.138 -(* problem-type *)
1.139 -{given = ["function_term t","bound_variable bdv"],
1.140 - where_= [],
1.141 - find = ["derivative t'"],
1.142 - with_ = ["t' is_derivative_of (%bdv. t)"],
1.143 - relate= []};
1.144 -(*the ' in t' is used to transfer the identifier from function_term*)
1.145 -
1.146 -
1.147 -(* ["equation","univariate"] *)
1.148 -(* ------------------------- *)
1.149 -(* problem-type *)
1.150 -{given = ["equality (lhs = rhs)",
1.151 - "bound_variable v","error_bound eps"],
1.152 - where_= [],
1.153 - find = ["solutions S"],
1.154 - with_ = ["ALL s. s : S --> || (%v. lhs) s - (%v. rhs) s || <= eps"],
1.155 - relate= []};
1.156 -
1.157 -
1.158 -(* find-values *)
1.159 -(* ----------- *)
1.160 -(* problem-type *)
1.161 -{given = ["max_relation r","additional_relations RS"],
1.162 - where_= [],
1.163 - find = ["values_for VS"],
1.164 - with_ = [(*???*)],
1.165 - relate= []};
1.166 -
1.167 -(* (1) variant of instantiation *)
1.168 -{given = ["max_relation (A = a*b)",
1.169 - "additional_relations [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]"],
1.170 - where_= [],
1.171 - find = ["values_for [a,b]"],
1.172 - with_ = [],
1.173 - relate= []};
1.174 -
1.175 -(* (2) variant of instantiation *)
1.176 -{given = ["max_relation (A = a*b)",],
1.177 - where_= [],
1.178 - find = ["values_for [A]",
1.179 - "additional_relations [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
1.180 - with_ = [],
1.181 - relate= []};
1.182 -
1.183 -(*
1.184 -(3) data-transfer between the the hidden formalization,
1.185 - the root-problem and the sub-problems;
1.186 -
1.187 -maximum -> #given.make-fun
1.188 --------------------
1.189 -maximum.#relate "max_relation r" -> "equality (lhs = rhs)"
1.190 -formalization "bound_variable v" -> "bound_variable v"
1.191 -maximum.#relate "additional_relations RS"-> "equalities es"
1.192 -
1.193 -
1.194 -maximum + make-fun -> #given.max-of-fun-on-interval
1.195 ---------------------------------------------
1.196 -make-fun.#find "function_term lhs_" -> "function_term t"
1.197 -make-fun.#given "bound_variable v" -> "bound_variable v"
1.198 -formalization -> "domain {x::real. ...}"
1.199 -
1.200 -
1.201 -max-of-fun-on-interval -> #given.derivative
1.202 -------------------------------------
1.203 -make-fun.#find "function_term lhs_" -> "function_term t"
1.204 -make-fun.#given "bound_variable v" -> "bound_variable bdv"
1.205 -
1.206 -
1.207 -max-of-fun-on-interval + derivative ->
1.208 - #given.["equation","univariate"]
1.209 -----------------------------------------------------------------
1.210 -derivative.#find "derivative t'" -> "equality (lhs = rhs)"
1.211 - (* t'= #0 *)
1.212 -make-fun.#given "bound_variable v" -> "bound_variable v"
1.213 -formalization -> "error_bound eps"
1.214 -
1.215 -
1.216 -maximum + make-fun + max-of-fun-on-interval -> #given.find-values
1.217 -----------------------------------------------------------
1.218 -maximum.#relate "max_relation r" -> "max_relation r"
1.219 -maximum.#relate "additional_relations RS"-> "additional_relations RS"
1.220 -*)
1.221 -
1.222 -
1.223 -
1.224 -
1.225 -(* vvv--- geht nicht wegen fun-types
1.226 -parse thy "case maxmin of is_max => (m' <= m) | is_min => (m <= m')";
1.227 -parse thy "if maxmin = is_max then (m' <= m) else (m <= m')";
1.228 -parse thy "if a=b then a else b";
1.229 -parse thy "maxmin = is_max";
1.230 -parse thy "maxmin =!= is_max";
1.231 - ^^^--- geht nicht wegen fun-types *)
1.232 -
1.233 -"pbltyp --- maximum ---";
1.234 -val pbltyp = {given=["fixed_values (cs::bool list)"],
1.235 - where_=["foldl (op &) True (map is_equality cs)",
1.236 - "foldl (op &) True (map (Not o ((op <=) #0) o Rhs) cs)"],
1.237 - find=["maximum m","values_for (ms::real list)"],
1.238 - with_=["Ex_frees ((foldl (op &) True (r#rs)) & \
1.239 - \ (ALL m'. (subst (m,m') (foldl (op &) True (r#rs)) \
1.240 - \ --> m' <= m)))"],
1.241 - relate=["max_relation r","additional_relations rs"]}:string ppc;
1.242 -val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
1.243 -"coil";
1.244 -val org = ["fixed_values [R=(R::real)]",
1.245 - "bound_variable a", "bound_variable b", "bound_variable alpha",
1.246 - "domain {x::real. #0 <= x & x <= #2*R}",
1.247 - "domain {x::real. #0 <= x & x <= #2*R}",
1.248 - "domain {x::real. #0 <= x & x <= pi}",
1.249 - "maximum A",
1.250 - "max_relation A=#2*a*b - a^^^#2",
1.251 - "additional_relations [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
1.252 - "additional_relations [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
1.253 - "additional_relations [a=#2*R*sin alpha, b=#2*R*cos alpha]"];
1.254 -val chkorg = map (the o (parse thy)) org;
1.255 -val pbl = {given=["fixed_values [R=(R::real)]"],where_=[],
1.256 - find=["maximum A","values_for [a,b]"],
1.257 - with_=["EX alpha. A=#2*a*b - a^^^#2 & \
1.258 - \ a=#2*R*sin alpha & b=#2*R*cos alpha & \
1.259 - \ (ALL A'. A'=#2*a*b - a^^^#2 & a=#2*R*sin alpha & b=#2*R*cos alpha \
1.260 - \ --> A' <= A)"],
1.261 - relate=["max_relation (A=#2*a*b - a^^^#2)",
1.262 - "additional_relations [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
1.263 - }: string ppc;
1.264 -val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
1.265 -
1.266 -"met --- maximum_by_differentiation ---";
1.267 -val met = {given=["fixed_values (cs::bool list)","bound_variable v",
1.268 - "domain {x::real. lower_bound <= x & x <= upper_bound}",
1.269 - "approximation apx"],
1.270 - where_=[],
1.271 - find=["maximum m","values_for (ms::real list)",
1.272 - "function_term t","max_argument mx"],
1.273 - with_=["Ex_frees ((foldl (op &) True (rs::bool list)) & \
1.274 - \ (ALL m'. (subst (m,m') (foldl (op &) True rs) \
1.275 - \ --> m' <= m))) & \
1.276 - \m = (%v. t) mx & \
1.277 - \( ALL x. lower_bound <= x & x <= upper_bound \
1.278 - \ --> (%v. t) x <= m)"],
1.279 - relate=["rs::bool list"]}: string ppc;
1.280 -val chkpbl = ((map (the o (parse thy))) o ppc2list) met;
1.281 -
1.282 -
1.283 -"pbltyp --- make_fun ---";
1.284 -(* subproblem [(hd #relate root, equality),
1.285 - (bound_variable formalization, bound_variable),
1.286 - (tl #relate root, equalities)] *)
1.287 -val pbltyp = {given=["equality e","bound_variable v", "equalities es"],
1.288 - where_=[],
1.289 - find=["function_term t"],with_=[(*???*)],
1.290 - relate=[(*???*)]}: string ppc;
1.291 -val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
1.292 -"coil";
1.293 -val pbl = {given=["equality (A=#2*a*b - a^^^#2)","bound_variable alpha",
1.294 - "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
1.295 - where_=[],
1.296 - find=["function_term t"],
1.297 - with_=[],relate=[]}: string ppc;
1.298 -val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
1.299 -
1.300 -"met --- make_explicit_and_substitute ---";
1.301 -val met = {given=["equality e","bound_variable v", "equalities es"],
1.302 - where_=[],
1.303 - find=["function_term t"],with_=[(*???*)],
1.304 - relate=[(*???*)]}: string ppc;
1.305 -val chkmet = ((map (the o (parse thy))) o ppc2list) met;
1.306 -"met --- introduce_a_new_variable ---";
1.307 -val met = {given=["equality e","bound_variable v", "substitutions es"],
1.308 - where_=[],
1.309 - find=["function_term t"],with_=[(*???*)],
1.310 - relate=[(*???*)]}: string ppc;
1.311 -val chkmet = ((map (the o (parse thy))) o ppc2list) met;
1.312 -
1.313 -
1.314 -"pbltyp --- max_of_fun_on_interval ---";
1.315 -val pbltyp = {given=["function_term t","bound_variable v",
1.316 - "domain {x::real. lower_bound <= x & x <= upper_bound}"],
1.317 - where_=[],
1.318 - find=["maximums ms"],
1.319 - with_=["ALL m. m : ms --> \
1.320 - \ (ALL x::real. lower_bound <= x & x <= upper_bound \
1.321 - \ --> (%v. t) x <= m)"],
1.322 - relate=[]}: string ppc;
1.323 -val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
1.324 -"coil";
1.325 -val pbl = {given=["function_term #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \
1.326 - \ (#2*R*sin alpha)^^^#2","bound_variable alpha",
1.327 - "domain {x::real. #0 <= x & x <= pi}"],where_=[],
1.328 - find=["maximums [#1234]"],with_=[],relate=[]}: string ppc;
1.329 -val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
1.330 -
1.331 -
1.332 -(* pbltyp --- max_of_fun --- *)
1.333 -(*
1.334 -{given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;
1.335 -val (SOME ct) = parse thy ;
1.336 -atomty thy (term_of ct);
1.337 -*)
1.338 -
1.339 -
1.340 -
1.341 -
1.342 -
1.343 -
1.344 -
1.345 -
1.346 -(* --- 14.1.00 --- *)
1.347 -"p.114";
1.348 -val org = {given=["[u=(#12::real)]"],where_=[],
1.349 - find=["[a,(b::real)]"],with_=[],
1.350 - relate=["[is_max A=a*(b::real), #2*a+#2*b=(u::real)]"]}: string ppc;
1.351 -val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.352 -"p.116";
1.353 -val org = {given=["[c=#10, h=(#4::real)]"],where_=[],
1.354 - find=["[x,(y::real)]"],with_=[],
1.355 - relate=["[A=x*(y::real), c//h=x//(h-(y::real))]"]}: string ppc;
1.356 -val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.357 -"p.117";
1.358 -val org = {given=["[r=#5]"],where_=[],
1.359 - find=["[x,(y::real)]"],with_=[],
1.360 - relate=["[is_max #0=pi*x^^^#2 + pi*x*(r::real)]"]}: string ppc;
1.361 -val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.362 -"#241";
1.363 -val org = {given=["[s=(#10::real)]"],where_=[],
1.364 - find=["[p::real]"],with_=[],
1.365 - relate=["[is_max p=n*m, s=n+(m::real)]"]}: string ppc;
1.366 -val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.367 -
1.368 -(*
1.369 -{given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;
1.370 -val (SOME ct) = parse thy ;
1.371 -atomty thy (term_of ct);
1.372 -*)