1.1 --- a/src/Tools/isac/IsacKnowledge/DiffApp-scrpbl.sml Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,429 +0,0 @@
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 (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) 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) 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) 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) 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) 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) 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") *)