1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/IsacKnowledge/DiffApp-scrpbl.sml Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,429 @@
1.4 +(* use"test-coil-kernel.sml";
1.5 + W.N.22.11.99
1.6 +
1.7 +*)
1.8 +
1.9 +(* vvv--- geht nicht wegen fun-types
1.10 +parse thy "case maxmin of is_max => (m' <= m) | is_min => (m <= m')";
1.11 +parse thy "if maxmin = is_max then (m' <= m) else (m <= m')";
1.12 +parse thy "if a=b then a else b";
1.13 +parse thy "maxmin = is_max";
1.14 +parse thy "maxmin =!= is_max";
1.15 + ^^^--- geht nicht wegen fun-types *)
1.16 +
1.17 +"pbltyp --- maximum ---";
1.18 +val pbltyp = {given=["fixedValues (cs::bool list)"],
1.19 + where_=[(*"foldl (op &) True (map is_equality cs)",
1.20 + "foldl (op &) True (map (Not o ((op <=) #0) o Rhs) cs)"*)],
1.21 + find=["maximum m","values_for (ms::real list)"],
1.22 + with_=[(*"Ex_frees ((foldl (op &) True (r#rs)) & \
1.23 + \ (ALL m'. (subst (m,m') (foldl (op &) True (r#rs)) \
1.24 + \ --> m' <= m)))"*)],
1.25 + relate=["max_relation r","additionalRels rs"]}:string ppc;
1.26 +val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
1.27 +"coil";
1.28 +val org = ["fixedValues [R=(R::real)]",
1.29 + "boundVariable a","boundVariable b","boundVariable alpha",
1.30 + "domain {x::real. #0 <= x & x <= #2*R}",
1.31 + "domain {x::real. #0 <= x & x <= #2*R}",
1.32 + "domain {x::real. #0 <= x & x <= pi}",
1.33 + "errorBound (eps = #1//#1000)",
1.34 + "maximum A",
1.35 + (*"max_relation A=#2*a*b - a^^^#2",*)
1.36 + "relations [A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
1.37 + "relations [A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
1.38 + "relations [A=#2*a*b - a^^^#2, a=#2*R*sin alpha, b=#2*R*cos alpha]"];
1.39 +val chkorg = map (the o (parse thy)) org;
1.40 +val pbl = {given=["fixedValues [R=(R::real)]"],where_=[],
1.41 + find=["maximum A","values_for [a,b]"],
1.42 + with_=[(* incompat.w. parse, ok with parseold
1.43 + "EX alpha. A=#2*a*b - a^^^#2 & \
1.44 + \ a=#2*R*sin alpha & b=#2*R*cos alpha & \
1.45 + \ (ALL A'. A'=#2*a*b - a^^^#2 & a=#2*R*sin alpha \
1.46 + \ & b=#2*R*cos alpha \
1.47 + \ --> A' <= A)"*)],
1.48 + relate=["relations [A=#2*a*b - a^^^#2, a=#2*R*sin alpha, b=#2*R*cos alpha]"]
1.49 + }: string ppc;
1.50 +val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
1.51 +
1.52 +"met --- maximum_by_differentiation ---";
1.53 +val met = {given=["fixedValues (cs::bool list)","boundVariable v",
1.54 + "domain {x::real. lower_bound <= x & x<=upper_bound}",
1.55 + "errorBound epsilon"],
1.56 + where_=[],
1.57 + find=["maximum m","valuesFor (ms::bool list)",
1.58 + "function_term t","max_argument mx"],
1.59 + with_=[(* incompat.w. parse, ok with parseold
1.60 + "Ex_frees ((foldl (op &) True (mr#ars)) & \
1.61 + \ (ALL m'. (subst (m,m') (foldl (op &) True (mr#ars))\
1.62 + \ --> m' <= m))) & \
1.63 + \m = (%v. t) mx & \
1.64 + \( ALL x. lower_bound <= x & x <= upper_bound \
1.65 + \ --> (%v. t) x <= m)"*)],
1.66 + relate=["max_relation mr",
1.67 + "additionalRels ars"]}: string ppc;
1.68 +val chkpbl = ((map (the o (parse thy))) o ppc2list) met;
1.69 +
1.70 +"data --- maximum_by_differentiation ---";
1.71 +val met = {given=["fixedValues [R=(R::real)]","boundVariable alpha",
1.72 + "domain {x::real. #0 <= x & x <= pi//#2}",
1.73 + "errorBound (eps = #1//#1000)"],
1.74 + where_=[],
1.75 + find=["maximum A","valuesFor [a=Undef]",
1.76 + "function_term t","max_argument mx"],
1.77 + with_=[(* incompat.w. parse, ok with parseold
1.78 + "EX b alpha. A = #2*a*b - a^^^#2 & \
1.79 + \ a = #2*R*sin alpha & \
1.80 + \ b = #2*R*cos alpha & \
1.81 + \ (ALL A'. A'= #2*a*b - a^^^#2 & \
1.82 + \ a = #2*R*sin alpha & \
1.83 + \ b = #2*R*cos alpha --> A' <= A) & \
1.84 + \ A = (%alpha. t) mx & \
1.85 + \ (ALL x. #0 <= x & x <= pi --> \
1.86 + \ (%alpha. t) x <= A)"*)],
1.87 + relate=["max_relation mr",
1.88 + "additionalRels ars"]}: string ppc;
1.89 +val chkpbl = ((map (the o (parse thy))) o ppc2list) met;
1.90 +
1.91 +val (Some ct) = parseold thy "EX b. (EX alpha. A = #2*a*b - a^^^#2)";
1.92 +
1.93 +"pbltyp --- make_fun ---";
1.94 +(* subproblem [(hd #relate root, equality),
1.95 + (boundVariable formalization, boundVariable),
1.96 + (tl #relate root, equalities)] *)
1.97 +val pbltyp = {given=["equality e","boundVariable v", "equalities es"],
1.98 + where_=[],
1.99 + find=["functionTerm t"],with_=[(*???*)],
1.100 + relate=[(*???*)]}: string ppc;
1.101 +val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
1.102 +"coil";
1.103 +val pbl = {given=["equality (A=#2*a*b - a^^^#2)","boundVariable alpha",
1.104 + "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
1.105 + where_=[],
1.106 + find=["functionTerm t"],
1.107 + with_=[],relate=[]}: string ppc;
1.108 +val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
1.109 +
1.110 +"met --- make_explicit_and_substitute ---";
1.111 +val met = {given=["equality e","boundVariable v", "equalities es"],
1.112 + where_=[],
1.113 + find=["functionTerm t"],with_=[(*???*)],
1.114 + relate=[(*???*)]}: string ppc;
1.115 +val chkmet = ((map (the o (parse thy))) o ppc2list) met;
1.116 +"met --- introduce_a_new_variable ---";
1.117 +val met = {given=["equality e","boundVariable v", "substitutions es"],
1.118 + where_=[],
1.119 + find=["functionTerm t"],with_=[(*???*)],
1.120 + relate=[(*???*)]}: string ppc;
1.121 +val chkmet = ((map (the o (parse thy))) o ppc2list) met;
1.122 +
1.123 +
1.124 +"pbltyp --- max_of_fun_on_interval ---";
1.125 +val pbltyp = {given=["functionTerm t","boundVariable v",
1.126 + "domain {x::real. lower_bound <= x & x <= upper_bound}"],
1.127 + where_=[],
1.128 + find=["maximums ms"],
1.129 + with_=[(* incompat.w. parse, ok with parseold
1.130 + "ALL m. m : ms --> \
1.131 + \ (ALL x::real. lower_bound <= x & x <= upper_bound \
1.132 + \ --> (%v. t) x <= m)"*)],
1.133 + relate=[]}: string ppc;
1.134 +val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
1.135 +"coil";
1.136 +val pbl = {given=["functionTerm (f = #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \
1.137 + \ (#2*R*sin alpha)^^^#2)","boundVariable alpha",
1.138 + "domain {x::real. #0 <= x & x <= pi}"],where_=[],
1.139 + find=["maximums [#1234]"],with_=[],relate=[]}: string ppc;
1.140 +val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
1.141 +
1.142 +
1.143 +(* pbltyp --- max_of_fun --- *)
1.144 +(*
1.145 +{given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;
1.146 +val (Some ct) = parse thy ;
1.147 +atomty thy (term_of ct);
1.148 +*)
1.149 +
1.150 +
1.151 +(* --- 14.1.00 ev. nicht ganz up to date bzg. oberem --- *)
1.152 +"p.114";
1.153 +val org = {given=["[u=(#12::real)]"],where_=[],
1.154 + find=["[a,(b::real)]"],with_=[],
1.155 + relate=["[is_max A=a*(b::real), #2*a+#2*b=(u::real)]"]}: string ppc;
1.156 +val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.157 +"p.116";
1.158 +val org = {given=["[c=#10, h=(#4::real)]"],where_=[],
1.159 + find=["[x,(y::real)]"],with_=[],
1.160 + relate=["[A=x*(y::real), c//h=x//(h-(y::real))]"]}: string ppc;
1.161 +val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.162 +"p.117";
1.163 +val org = {given=["[r=#5]"],where_=[],
1.164 + find=["[x,(y::real)]"],with_=[],
1.165 + relate=["[is_max #0=pi*x^^^#2 + pi*x*(r::real)]"]}: string ppc;
1.166 +val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.167 +"#241";
1.168 +val org = {given=["[s=(#10::real)]"],where_=[],
1.169 + find=["[p::real]"],with_=[],
1.170 + relate=["[is_max p=n*m, s=n+(m::real)]"]}: string ppc;
1.171 +val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.172 +
1.173 +
1.174 +
1.175 +(* -------------- coil-kernel -------------- vor 19.1.00 *)
1.176 +(* --- subproblem: make-function-by-subst ~~~~~~~~~~~ *)
1.177 +(* --- subproblem: max-of-function *)
1.178 +(* --- subproblem: derivative *)
1.179 +(* --- subproblem: tan-quadrat-equation *)
1.180 +"-------------- coil-kernel --------------";
1.181 +val origin = ["A=#2*a*b - a^^^#2",
1.182 + "a::real","b::real","{x. #0<x & x<R//#2}",
1.183 + "{(a//#2)^^^#2 + (b//#2)^^^#2 = (R//#2)^^^#2}",
1.184 + "alpha::real","{alpha::real. #0<alpha & alpha<pi//#2}",
1.185 + "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",
1.186 + "{R::real}"];
1.187 +(* --- for a isa-users-mail --- FIXME
1.188 +Goal "{x. x < a} = ?z";
1.189 +{x::'a. x < a} = ?z
1.190 +Goal "{x. x < #3} = {a}";
1.191 +{x::'a. x < (#3::'a)} = {a}
1.192 +Goal "{x. #3 < x} = ?z";
1.193 +Collect (op < (#3::'a)) = ?z
1.194 +---------------------------- *)
1.195 +
1.196 +val formals = map (the o (parse thy)) origin;
1.197 +
1.198 +val given = ["formula_for_max (lhs=rhs)","boundVariable bdv",
1.199 + "interval {x. low < x & x < high}",
1.200 + "additional_conds ac","constants cs"];
1.201 +val where_ = ["lhs is_const","bdv is_const","low is_const","high is_const",
1.202 + "||| Vars equ ||| = ||| VarsSet ac ||| - ||| ac ||| + #1"];
1.203 +val find = ["f::real => real","maxs::real set"];
1.204 +val with_ = [(* incompat.w. parse, ok with parseold
1.205 + "maxs = {m. low < m & m < high & \
1.206 + \ (m is_local_max_of (%bdv. f))}"*)];
1.207 +val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1.208 +val givens = map (the o (parse thy)) given;
1.209 +
1.210 +"------- 1.1 -------";
1.211 +(* 5.3.00
1.212 +val formals = map (the o (parse thy)) ["A=#2*a*b - a^^^#2",
1.213 + "a::real","{x. #0<x & x<R//#2}",
1.214 + "{(a//#2)^^^#2 + (b//#2)^^^#2 = (R//#2)^^^#2}",
1.215 + "{R::real}"];
1.216 +val tag__forms = chktyps thy (formals, givens);
1.217 +map ((atomty thy) o term_of) tag__forms;
1.218 +
1.219 +val formals = map (the o (parse thy)) ["A=#2*a*b - a^^^#2",
1.220 + "alpha::real","{alpha. #0<alpha & alpha<pi//#2}",
1.221 + "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",
1.222 + "{R::real}"];
1.223 +val tag__forms = chktyps thy (formals, givens);
1.224 +map ((atomty thy) o term_of) tag__forms;
1.225 +*)
1.226 +
1.227 +" --- subproblem: make-function-by-subst --- ";
1.228 +val origin = ["A=#2*a*b - a^^^#2",
1.229 + "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",
1.230 + "{R::real}"];
1.231 +val formals = map (the o (parse thy)) origin;
1.232 +
1.233 +val given = ["equation (lhs=rhs)","substitutions ss",
1.234 + "constants cs"];
1.235 +val where_ = [];
1.236 +val find = ["t::real"];
1.237 +val with_ = ["||| Vars t ||| = #1"];
1.238 +val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1.239 +val givens = map (the o (parse thy)) given;
1.240 +(* 5.3.00
1.241 +val tag__forms = chktyps thy (formals, givens);
1.242 +map ((atomty thy) o term_of) tag__forms;
1.243 +*)
1.244 +" --- subproblem: max-of-function --- ";
1.245 +val origin = ["A = #2*(#2*R*(sin alpha))*(#2*R*(sin alpha)) - \
1.246 + \ (#2*R*(sin alpha))^^^#2",
1.247 + "{alpha. #0<alpha & alpha<pi//#2}",
1.248 + "{R::real}"];
1.249 +val formals = map (the o (parse thy)) origin;
1.250 +
1.251 +val given = ["equation (lhs=rhs)",
1.252 + "interval {x. low < x & x < high}",
1.253 + "constants cs"];
1.254 +val where_ = ["lhs is_const","low is_const","high is_const"];
1.255 +val find = ["t::real"];
1.256 +val with_ = ["||| Vars t ||| = #1"];
1.257 +val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1.258 +val givens = map (the o (parse thy)) given;
1.259 +(* 5.3.00
1.260 +val tag__forms = chktyps thy (formals, givens);
1.261 +map ((atomty thy) o term_of) tag__forms;
1.262 +*)
1.263 +" --- subproblem: derivative --- ";
1.264 +val origin = ["x^^^#3-y^^^#3+#-3*x+#12*y+#10","x::real"];
1.265 +val formals = map (the o (parse thy)) origin;
1.266 +
1.267 +val given = ["functionTerm t",
1.268 + "boundVariable bdv"];
1.269 +val where_ = ["bdv is_const"];
1.270 +val find = ["t'::real"];
1.271 +val with_ = ["t' is_derivative_of (%bdv. t)"];
1.272 +val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1.273 +val givens = map (the o (parse thy)) given;
1.274 +(*
1.275 +val tag__forms = chktyps thy (formals, givens);
1.276 +map ((atomty thy) o term_of) tag__forms;
1.277 +*)
1.278 +" --- subproblem: tan-quadrat-equation --- ";
1.279 +val origin = ["#8*R^^^#2*(cos alpha)^^^#2 + #-8*R^^^#2* \
1.280 + \ (cos alpha)*(sin alpha) + #8*R^^^#2*(sin alpha)^^^#2 = #0",
1.281 + "alpha::real","#1//#1000"];
1.282 +val formals = map (the o (parse thy)) origin;
1.283 +
1.284 +val given = ["equation (a*(cos bdv)^^^#2 + b*(cos bdv)*(sin bdv) + \
1.285 + \ c*(sin bdv) = #0)",
1.286 + "boundVariable bdv","errorBound epsilon"];
1.287 +val where_ = ["bdv is_const","epsilon is_const_expr"];
1.288 +val find = ["L::real set"];
1.289 +val with_ = ["L = {x. || (%bdv. a*(cos bdv)^^^#2 + b*(cos bdv)*(sin bdv) + \
1.290 + \ c*(sin bdv)) x || < epsilon}"];
1.291 +(* 5.3.00
1.292 +val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1.293 +val givens = map (the o (parse thy)) given;
1.294 +val tag__forms = chktyps thy (formals, givens);
1.295 +map ((atomty thy) o term_of) tag__forms;
1.296 +*)
1.297 +(* use"test-coil-kernel.sml";
1.298 + *)
1.299 +
1.300 +
1.301 +" #################################################### ";
1.302 +" test specify ";
1.303 +" #################################################### ";
1.304 +
1.305 +
1.306 +val cts =
1.307 +["fixedValues [R=(R::real)]",
1.308 + "boundVariable a", "boundVariable b",
1.309 + "boundVariable alpha",
1.310 + "domain {x::real. #0 <= x & x <= #2*R}",
1.311 + "domain {x::real. #0 <= x & x <= #2*R}",
1.312 + "domain {x::real. #0 <= x & x <= pi//#2}",
1.313 + "errorBound (eps = #1//#1000)",
1.314 + "maximum A","valuesFor [a=Undef]",
1.315 + (*"functionTerm t","max_argument mx",
1.316 + "max_relation (A=#2*a*b - a^^^#2)", *)
1.317 + "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
1.318 + "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
1.319 + "additionalRels [A=#2*a*b - a^^^#2,a=#2*R*sin alpha, b=#2*R*cos alpha]"];
1.320 +val (dI',pI',mI')=
1.321 + ("DiffAppl.thy",["Script.thy","maximum_of","function"],e_metID);
1.322 +val c = []:cid;
1.323 +
1.324 +(*
1.325 +val pbl = {given=["fixedValues [R=(R::real)]","boundVariable alpha",
1.326 + "domain {x::real. #0 <= x & x <= pi//#2}",
1.327 + "errorBound (eps = #1//#1000)"],
1.328 + where_=[],
1.329 + find=["maximum A","valuesFor [a=Undef]"(*,
1.330 + "functionTerm t","max_argument mx"*)],
1.331 + with_=[],
1.332 + relate=["max_relation (A=#2*a*b - a^^^#2)",
1.333 + "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
1.334 + "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
1.335 + "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
1.336 + }: string ppc;
1.337 +*)
1.338 +val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =
1.339 + specify (Init_Proof (cts,(dI',pI',mI'))) e_pos' [] EmptyPtree;
1.340 +
1.341 +val ct = "fixedValues [R=(R::real)]";
1.342 +(*l(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify(Add_Given ct) p c pt*)
1.343 +val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
1.344 +
1.345 +val ct = "boundVariable a";
1.346 +val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
1.347 +val ct = "boundVariable alpha";
1.348 +val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
1.349 +
1.350 +val ct = "domain {x::real. #0 <= x & x <= pi//#2}";
1.351 +val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
1.352 +
1.353 +val ct = "errorBound (eps = (#1::real) // #1000)";
1.354 +val ct = "maximum A";
1.355 +val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
1.356 +
1.357 +val ct = "valuesFor [a=Undef]";
1.358 +val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
1.359 +
1.360 +val ct = "max_relation ()";
1.361 +val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
1.362 +
1.363 +val ct = "relations [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]";
1.364 +val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
1.365 +
1.366 +(* ... nxt = Specify_Domain ...
1.367 +val ct = "additionalRels [b=#2*R*cos alpha]";
1.368 +val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =
1.369 + specify(Add_Relation ct) p c pt;
1.370 +(*
1.371 +val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
1.372 +*)
1.373 +val ct = "additionalRels [a=#2*R*sin alpha]";
1.374 +val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =
1.375 + specify(Add_Relation ct) p c pt;
1.376 +(*
1.377 +val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
1.378 +*)
1.379 +*)
1.380 +(* --- tricky case (termlist interleaving variants):
1.381 +> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =
1.382 + specify (Init_Proof (cts,(dI,pI,mI))) [] [] EmptyPtree;
1.383 +
1.384 +> val ct = "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2, b=#2*R*cos alpha]";
1.385 +> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
1.386 +*)
1.387 +
1.388 +(* --- incomplete input ---
1.389 +> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =
1.390 + specify (Init_Proof (cts,(dI,pI,mI))) [] [] EmptyPtree;
1.391 +
1.392 +> val ct = "[R=(R::real)]";
1.393 +> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
1.394 +
1.395 +> val ct = "R=(R::real)";
1.396 +> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
1.397 +
1.398 +> val ct = "(R::real)";
1.399 +> specify nxt p c pt;
1.400 +*)
1.401 +
1.402 +
1.403 +" #################################################### ";
1.404 +" test do_ specify ";
1.405 +" #################################################### ";
1.406 +
1.407 +
1.408 +val cts = ["fixedValues [R=(R::real)]",
1.409 + "boundVariable a", "boundVariable b",
1.410 + "boundVariable alpha",
1.411 + "domain {x::real. #0 <= x & x <= #2*R}",
1.412 + "domain {x::real. #0 <= x & x <= #2*R}",
1.413 + "domain {x::real. #0 <= x & x <= pi//#2}",
1.414 + "errorBound (eps=#1//#1000)",
1.415 + "maximum A","valuesFor [a=Undef]",
1.416 + (*"functionTerm t","max_argument mx", *)
1.417 + "max_relation (A=#2*a*b - a^^^#2)",
1.418 + "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
1.419 + "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
1.420 + "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"];
1.421 +val (dI',pI',mI')=
1.422 + ("DiffAppl.thy",["DiffAppl.thy","test_maximum"],e_metID);
1.423 +val p = e_pos'; val c = [];
1.424 +
1.425 +val (mI,m) = ("Init_Proof",Init_Proof (cts, (dI',pI',mI')));
1.426 +val (pst as (sc,pt,cl):pstate) = (EmptyScr, e_ptree, []);
1.427 +val (p,_,f,nxt,_,(_,pt,_)) = do_ (mI,m) p c pst;
1.428 +(*val nxt = ("Add_Given",Add_Given "fixedValues [R = R]")*)
1.429 +
1.430 +val (p,_,Form' (PpcKF (_,_,ppc)),nxt,_,(_,pt,_)) =
1.431 + do_ nxt p c (EmptyScr,pt,[]);
1.432 +(*val nxt = ("Add_Given",Add_Given "boundVariable a") *)