neuper@37906: (* use"test-coil-kernel.sml";
neuper@37906:    W.N.22.11.99
neuper@37906:    
neuper@37906: *)
neuper@37906: 
neuper@37906: (* vvv--- geht nicht wegen fun-types
neuper@37906: parse thy "case maxmin of is_max => (m' <= m) | is_min => (m <= m')";
neuper@37906: parse thy "if maxmin = is_max then (m' <= m) else (m <= m')";
neuper@37906: parse thy "if a=b then a else b";
neuper@37906: parse thy "maxmin = is_max";
neuper@37906: parse thy "maxmin =!= is_max";
neuper@37906:    ^^^--- geht nicht wegen fun-types *)
neuper@37906: 
neuper@37906: "pbltyp --- maximum ---";
neuper@37906: val pbltyp = {given=["fixedValues (cs::bool list)"],
neuper@37906: 	      where_=[(*"foldl (op &) True (map is_equality cs)",
neuper@37906: 		      "foldl (op &) True (map (Not o ((op <=) #0) o Rhs) cs)"*)],
neuper@37906: 	      find=["maximum m","values_for (ms::real list)"],
neuper@37906: 	      with_=[(*"Ex_frees ((foldl (op &) True (r#rs)) &              \
neuper@37906:                       \ (ALL m'. (subst (m,m') (foldl (op &) True (r#rs)) \
neuper@37906: 		      \            --> m' <= m)))"*)],
neuper@37906: 	      relate=["max_relation r","additionalRels rs"]}:string ppc;
neuper@37906: val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
neuper@37906: "coil";
neuper@37906: val org = ["fixedValues [R=(R::real)]", 
neuper@37906: 	   "boundVariable a","boundVariable b","boundVariable alpha",
neuper@37906: 	   "domain {x::real. #0 <= x & x <= #2*R}",
neuper@37906: 	   "domain {x::real. #0 <= x & x <= #2*R}",
neuper@37906: 	   "domain {x::real. #0 <= x & x <= pi}",
neuper@37906: 	   "errorBound (eps = #1//#1000)",
neuper@37906: 	   "maximum A",
neuper@37906: 	 (*"max_relation A=#2*a*b - a^^^#2",*)
neuper@37906: 	   "relations [A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
neuper@37906: 	   "relations [A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
neuper@37906: 	   "relations [A=#2*a*b - a^^^#2, a=#2*R*sin alpha, b=#2*R*cos alpha]"];
neuper@37906: val chkorg = map (the o (parse thy)) org;
neuper@37906: val pbl = {given=["fixedValues [R=(R::real)]"],where_=[],
neuper@37906: 	   find=["maximum A","values_for [a,b]"],
neuper@37906: 	   with_=[(* incompat.w. parse, ok with parseold
neuper@37906: 		   "EX alpha. A=#2*a*b - a^^^#2 &    \
neuper@37906: 	    \ a=#2*R*sin alpha & b=#2*R*cos alpha & \
neuper@37906: 	    \ (ALL A'. A'=#2*a*b - a^^^#2 & a=#2*R*sin alpha \
neuper@37906: 	    \          & b=#2*R*cos alpha \
neuper@37906: 	    \         --> A' <= A)"*)],
neuper@37906: 	   relate=["relations [A=#2*a*b - a^^^#2, a=#2*R*sin alpha, b=#2*R*cos alpha]"]
neuper@37906: 	  }: string ppc;
neuper@37906: val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
neuper@37906: 
neuper@37906: "met --- maximum_by_differentiation ---";
neuper@37906: val met = {given=["fixedValues (cs::bool list)","boundVariable v",
neuper@37906: 		  "domain {x::real. lower_bound <= x & x<=upper_bound}",
neuper@37906: 		  "errorBound epsilon"],
neuper@37906: 	   where_=[],
neuper@37906: 	   find=["maximum m","valuesFor (ms::bool list)",
neuper@37906: 		 "function_term t","max_argument mx"],
neuper@37906: 	   with_=[(* incompat.w. parse, ok with parseold
neuper@37906: 		   "Ex_frees ((foldl (op &) True (mr#ars)) &           \
neuper@37906:                   \ (ALL m'. (subst (m,m') (foldl (op &) True (mr#ars))\
neuper@37906: 		  \            --> m' <= m))) &                        \
neuper@37906: 		  \m = (%v. t) mx &                                    \
neuper@37906:                   \( ALL x. lower_bound <= x & x <= upper_bound        \
neuper@37906: 	          \       --> (%v. t) x <= m)"*)],
neuper@37906: 	   relate=["max_relation mr",
neuper@37906: 		   "additionalRels ars"]}: string ppc;
neuper@37906: val chkpbl = ((map (the o (parse thy))) o ppc2list) met;
neuper@37906: 
neuper@37906: "data --- maximum_by_differentiation ---";
neuper@37906: val met = {given=["fixedValues [R=(R::real)]","boundVariable alpha",
neuper@37906: 		  "domain {x::real. #0 <= x & x <= pi//#2}",
neuper@37906: 		  "errorBound (eps = #1//#1000)"],
neuper@37906: 	   where_=[],
neuper@37906: 	   find=["maximum A","valuesFor [a=Undef]",
neuper@37906: 		 "function_term t","max_argument mx"],
neuper@37906: 	   with_=[(* incompat.w. parse, ok with parseold
neuper@37906: 		   "EX b alpha. A = #2*a*b - a^^^#2 &     \
neuper@37906: 	            \          a = #2*R*sin alpha  &     \
neuper@37906: 		    \          b = #2*R*cos alpha  &     \
neuper@37906: 		    \ (ALL A'. A'= #2*a*b - a^^^#2 &     \
neuper@37906: 	            \          a = #2*R*sin alpha  &     \
neuper@37906: 		    \          b = #2*R*cos alpha  --> A' <= A) & \
neuper@37906: 		    \ A = (%alpha. t) mx &               \
neuper@37906: 		    \ (ALL x. #0 <= x & x <= pi -->      \
neuper@37906:                     \          (%alpha. t) x <= A)"*)],
neuper@37906: 	   relate=["max_relation mr",
neuper@37906: 		   "additionalRels ars"]}: string ppc;
neuper@37906: val chkpbl = ((map (the o (parse thy))) o ppc2list) met;
neuper@37906: 
neuper@37926: val (SOME ct) = parseold thy "EX b. (EX alpha. A = #2*a*b - a^^^#2)";
neuper@37906: 
neuper@37906: "pbltyp --- make_fun ---";
neuper@37906: (* subproblem [(hd #relate root, equality),
neuper@37906:                (boundVariable formalization, boundVariable),
neuper@37906: 	       (tl #relate root, equalities)] *) 
neuper@37906: val pbltyp = {given=["equality e","boundVariable v", "equalities es"],
neuper@37906: 	      where_=[],
neuper@37906: 	      find=["functionTerm t"],with_=[(*???*)],
neuper@37906: 	      relate=[(*???*)]}: string ppc;
neuper@37906: val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
neuper@37906: "coil";
neuper@37906: val pbl = {given=["equality (A=#2*a*b - a^^^#2)","boundVariable alpha",
neuper@37906: 		  "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
neuper@37906: 	   where_=[],
neuper@37906: 	   find=["functionTerm t"],
neuper@37906: 	   with_=[],relate=[]}: string ppc;
neuper@37906: val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
neuper@37906: 
neuper@37906: "met --- make_explicit_and_substitute ---";
neuper@37906: val met = {given=["equality e","boundVariable v", "equalities es"],
neuper@37906: 	   where_=[],
neuper@37906: 	   find=["functionTerm t"],with_=[(*???*)],
neuper@37906: 	   relate=[(*???*)]}: string ppc;
neuper@37906: val chkmet = ((map (the o (parse thy))) o ppc2list) met;
neuper@37906: "met --- introduce_a_new_variable ---";
neuper@37906: val met = {given=["equality e","boundVariable v", "substitutions es"],
neuper@37906: 	   where_=[],
neuper@37906: 	   find=["functionTerm t"],with_=[(*???*)],
neuper@37906: 	   relate=[(*???*)]}: string ppc;
neuper@37906: val chkmet = ((map (the o (parse thy))) o ppc2list) met;
neuper@37906: 
neuper@37906: 
neuper@37906: "pbltyp --- max_of_fun_on_interval ---";
neuper@37906: val pbltyp = {given=["functionTerm t","boundVariable v",
neuper@37906: 		     "domain {x::real. lower_bound <= x & x <= upper_bound}"],
neuper@37906: 	      where_=[],
neuper@37906: 	      find=["maximums ms"],
neuper@37906: 	      with_=[(* incompat.w. parse, ok with parseold
neuper@37906: 		   "ALL m. m : ms --> \
neuper@37906: 	          \  (ALL x::real. lower_bound <= x & x <= upper_bound \
neuper@37906: 	          \        --> (%v. t) x <= m)"*)],
neuper@37906: 	      relate=[]}: string ppc;
neuper@37906: val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
neuper@37906: "coil";
neuper@37906: val pbl = {given=["functionTerm (f = #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \
neuper@37906:                    \ (#2*R*sin alpha)^^^#2)","boundVariable alpha",
neuper@37906: 		  "domain {x::real. #0 <= x & x <= pi}"],where_=[],
neuper@37906: 	   find=["maximums [#1234]"],with_=[],relate=[]}: string ppc;
neuper@37906: val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
neuper@37906: 
neuper@37906: 
neuper@37906: (* pbltyp --- max_of_fun --- *)
neuper@37906: (*
neuper@37906: {given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;
neuper@37926: val (SOME ct) = parse thy ;
wneuper@59186: atomty (Thm.term_of ct);
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: (* --- 14.1.00 ev. nicht ganz up to date bzg. oberem --- *)
neuper@37906: "p.114";
neuper@37906: val org = {given=["[u=(#12::real)]"],where_=[],
neuper@37906: 	   find=["[a,(b::real)]"],with_=[],
neuper@37906: 	   relate=["[is_max A=a*(b::real), #2*a+#2*b=(u::real)]"]}: string ppc;
neuper@37906: val chkorg = ((map (the o (parse thy))) o ppc2list) org;
neuper@37906: "p.116";
neuper@37906: val org = {given=["[c=#10, h=(#4::real)]"],where_=[],
neuper@37906: 	   find=["[x,(y::real)]"],with_=[],
neuper@37906: 	   relate=["[A=x*(y::real), c//h=x//(h-(y::real))]"]}: string ppc;
neuper@37906: val chkorg = ((map (the o (parse thy))) o ppc2list) org;
neuper@37906: "p.117";
neuper@37906: val org = {given=["[r=#5]"],where_=[],
neuper@37906: 	   find=["[x,(y::real)]"],with_=[],
neuper@37906: 	   relate=["[is_max #0=pi*x^^^#2 + pi*x*(r::real)]"]}: string ppc;
neuper@37906: val chkorg = ((map (the o (parse thy))) o ppc2list) org;
neuper@37906: "#241";
neuper@37906: val org = {given=["[s=(#10::real)]"],where_=[],
neuper@37906: 	   find=["[p::real]"],with_=[],
neuper@37906: 	   relate=["[is_max p=n*m, s=n+(m::real)]"]}: string ppc;
neuper@37906: val chkorg = ((map (the o (parse thy))) o ppc2list) org;
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (* -------------- coil-kernel -------------- vor 19.1.00 *)
neuper@37906: (* --- subproblem: make-function-by-subst    ~~~~~~~~~~~ *)
neuper@37906: (* --- subproblem: max-of-function *)
neuper@37906: (* --- subproblem: derivative *)
neuper@37906: (* --- subproblem: tan-quadrat-equation *)
neuper@37906: "-------------- coil-kernel --------------";
neuper@37906: val origin = ["A=#2*a*b - a^^^#2",
neuper@37906: 	      "a::real","b::real","{x. #0<x & x<R//#2}",
neuper@37906: 	      "{(a//#2)^^^#2 + (b//#2)^^^#2 = (R//#2)^^^#2}",
neuper@37906: 	      "alpha::real","{alpha::real. #0<alpha & alpha<pi//#2}",
neuper@37906: 	      "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",
neuper@37906: 	      "{R::real}"];
neuper@37906: (* --- for a isa-users-mail --- FIXME
neuper@37906: Goal "{x. x < a} = ?z";
neuper@37906: {x::'a. x < a} = ?z
neuper@37906: Goal "{x. x < #3} = {a}";
neuper@37906: {x::'a. x < (#3::'a)} = {a}
neuper@37906: Goal "{x. #3 < x} = ?z";
neuper@37906: Collect (op < (#3::'a)) = ?z
neuper@37906: ---------------------------- *)
neuper@37906: 
neuper@37906: val formals = map (the o (parse thy)) origin;
neuper@37906: 
neuper@37906: val given  = ["formula_for_max (lhs=rhs)","boundVariable bdv",
neuper@37906: 	      "interval {x. low < x & x < high}",
neuper@37906: 	      "additional_conds ac","constants cs"];
neuper@37906: val where_ = ["lhs is_const","bdv is_const","low is_const","high is_const",
neuper@37906: 	      "||| Vars equ ||| = ||| VarsSet ac ||| - ||| ac ||| + #1"];
neuper@37906: val find   = ["f::real => real","maxs::real set"];
neuper@37906: val with_  = [(* incompat.w. parse, ok with parseold
neuper@37906: 		   "maxs = {m. low < m & m < high & \
neuper@37906:                         \ (m is_local_max_of (%bdv. f))}"*)];
neuper@37906: val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
neuper@37906: val givens = map (the o (parse thy)) given;
neuper@37906: 
neuper@37906: "------- 1.1 -------";
neuper@37906: (* 5.3.00
neuper@37906: val formals = map (the o (parse thy)) ["A=#2*a*b - a^^^#2",
neuper@37906: 	      "a::real","{x. #0<x & x<R//#2}",
neuper@37906: 	      "{(a//#2)^^^#2 + (b//#2)^^^#2 = (R//#2)^^^#2}",
neuper@37906: 	      "{R::real}"];
neuper@37906: val tag__forms = chktyps thy (formals, givens);
wneuper@59186: map ((atomty) o Thm.term_of) tag__forms;
neuper@37906: 
neuper@37906: val formals = map (the o (parse thy)) ["A=#2*a*b - a^^^#2",
neuper@37906: 	      "alpha::real","{alpha. #0<alpha & alpha<pi//#2}",
neuper@37906: 	      "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",
neuper@37906: 	      "{R::real}"];
neuper@37906: val tag__forms = chktyps thy (formals, givens);
wneuper@59186: map ((atomty) o Thm.term_of) tag__forms;
neuper@37906: *)
neuper@37906: 
neuper@37906: " --- subproblem: make-function-by-subst --- ";
neuper@37906: val origin = ["A=#2*a*b - a^^^#2",
neuper@37906: 	      "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",
neuper@37906: 	      "{R::real}"];
neuper@37906: val formals = map (the o (parse thy)) origin;
neuper@37906: 
neuper@37906: val given  = ["equation (lhs=rhs)","substitutions ss",
neuper@37906: 	      "constants cs"];
neuper@37906: val where_ = [];
neuper@37906: val find   = ["t::real"];
neuper@37906: val with_  = ["||| Vars t ||| = #1"];
neuper@37906: val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
neuper@37906: val givens = map (the o (parse thy)) given;
neuper@37906: (* 5.3.00
neuper@37906: val tag__forms = chktyps thy (formals, givens);
wneuper@59186: map ((atomty) o Thm.term_of) tag__forms;
neuper@37906: *)
neuper@37906: " --- subproblem: max-of-function --- ";
neuper@37906: val origin = ["A = #2*(#2*R*(sin alpha))*(#2*R*(sin alpha)) - \
neuper@37906:                \ (#2*R*(sin alpha))^^^#2",
neuper@37906: 	      "{alpha. #0<alpha & alpha<pi//#2}",
neuper@37906: 	      "{R::real}"];
neuper@37906: val formals = map (the o (parse thy)) origin;
neuper@37906: 
neuper@37906: val given  = ["equation (lhs=rhs)",
neuper@37906: 	      "interval {x. low < x & x < high}",
neuper@37906: 	      "constants cs"];
neuper@37906: val where_ = ["lhs is_const","low is_const","high is_const"];
neuper@37906: val find   = ["t::real"];
neuper@37906: val with_  = ["||| Vars t ||| = #1"];
neuper@37906: val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
neuper@37906: val givens = map (the o (parse thy)) given;
neuper@37906: (* 5.3.00
neuper@37906: val tag__forms = chktyps thy (formals, givens);
wneuper@59186: map ((atomty) o Thm.term_of) tag__forms;
neuper@37906: *)
neuper@37906: " --- subproblem: derivative --- ";
neuper@37906: val origin = ["x^^^#3-y^^^#3+#-3*x+#12*y+#10","x::real"];
neuper@37906: val formals = map (the o (parse thy)) origin;
neuper@37906: 
neuper@37906: val given  = ["functionTerm t",
neuper@37906: 	      "boundVariable bdv"];
neuper@37906: val where_ = ["bdv is_const"];
neuper@37906: val find   = ["t'::real"];
neuper@37906: val with_  = ["t' is_derivative_of (%bdv. t)"];
neuper@37906: val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
neuper@37906: val givens = map (the o (parse thy)) given;
neuper@37906: (*
neuper@37906: val tag__forms = chktyps thy (formals, givens);
wneuper@59186: map ((atomty) o Thm.term_of) tag__forms;
neuper@37906: *)
neuper@37906: " --- subproblem: tan-quadrat-equation --- ";
neuper@37906: val origin = ["#8*R^^^#2*(cos alpha)^^^#2 + #-8*R^^^#2* \
neuper@37906: 	      \ (cos alpha)*(sin alpha) + #8*R^^^#2*(sin alpha)^^^#2 = #0",
neuper@37906: 	      "alpha::real","#1//#1000"];
neuper@37906: val formals = map (the o (parse thy)) origin;
neuper@37906: 
neuper@37906: val given  = ["equation (a*(cos bdv)^^^#2 + b*(cos bdv)*(sin bdv) + \
neuper@37906: 	      \ c*(sin bdv) = #0)",
neuper@37906: 	     "boundVariable bdv","errorBound epsilon"];
neuper@37906: val where_ = ["bdv is_const","epsilon is_const_expr"];
neuper@37906: val find   = ["L::real set"];
neuper@37906: val with_  = ["L = {x. || (%bdv. a*(cos bdv)^^^#2 + b*(cos bdv)*(sin bdv) + \
neuper@37906: 	      \ c*(sin bdv)) x || < epsilon}"];
neuper@37906: (* 5.3.00
neuper@37906: val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
neuper@37906: val givens = map (the o (parse thy)) given;
neuper@37906: val tag__forms = chktyps thy (formals, givens);
wneuper@59186: map ((atomty) o Thm.term_of) tag__forms;
neuper@37906: *)
neuper@37906: (*  use"test-coil-kernel.sml";
neuper@37906:   *)
neuper@37906: 
neuper@37906: 
neuper@37906: " #################################################### ";
neuper@37906: "                       test specify                   ";
neuper@37906: " #################################################### ";
neuper@37906: 
neuper@37906: 
neuper@37906: val cts = 
neuper@37906: ["fixedValues [R=(R::real)]", 
neuper@37906:  "boundVariable a", "boundVariable b",
neuper@37906:  "boundVariable alpha",
neuper@37906:  "domain {x::real. #0 <= x & x <= #2*R}",
neuper@37906:  "domain {x::real. #0 <= x & x <= #2*R}",
neuper@37906:  "domain {x::real. #0 <= x & x <= pi//#2}",
neuper@37906:  "errorBound (eps = #1//#1000)",
neuper@37906:  "maximum A","valuesFor [a=Undef]",
neuper@37906:  (*"functionTerm t","max_argument mx", 
neuper@37906:   "max_relation (A=#2*a*b - a^^^#2)",      *)
neuper@37906:  "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", 
neuper@37906:  "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
neuper@37906:  "additionalRels [A=#2*a*b - a^^^#2,a=#2*R*sin alpha, b=#2*R*cos alpha]"];
neuper@37906: val (dI',pI',mI')=
neuper@37991:   ("DiffAppl",["Script","maximum_of","function"],e_metID);
neuper@37906: val c = []:cid;
neuper@37906: 
neuper@37906: (*
neuper@37906: val pbl = {given=["fixedValues [R=(R::real)]","boundVariable alpha",
neuper@37906: 		  "domain {x::real. #0 <= x & x <= pi//#2}",
neuper@37906: 		  "errorBound (eps = #1//#1000)"],
neuper@37906: 	   where_=[],
neuper@37906: 	   find=["maximum A","valuesFor [a=Undef]"(*,
neuper@37906: 		 "functionTerm t","max_argument mx"*)],
neuper@37906: 	   with_=[],
neuper@37906: 	   relate=["max_relation (A=#2*a*b - a^^^#2)",
neuper@37906: 	   "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", 
neuper@37906: 	   "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
neuper@37906: 	   "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
neuper@37906: 	   }: string ppc;
neuper@37906: *)
neuper@37906: val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = 
neuper@37906:   specify (Init_Proof (cts,(dI',pI',mI'))) e_pos' [] EmptyPtree;
neuper@37906: 
neuper@37906: val ct = "fixedValues [R=(R::real)]";
neuper@37906: (*l(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify(Add_Given ct) p c pt*)
neuper@37906: val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
neuper@37906: 
neuper@37906: val ct = "boundVariable a";
neuper@37906: val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
neuper@37906: val ct = "boundVariable alpha";
neuper@37906: val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
neuper@37906: 
neuper@37906: val ct = "domain {x::real. #0 <= x & x <= pi//#2}";
neuper@37906: val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
neuper@37906: 
neuper@37906: val ct = "errorBound (eps = (#1::real) // #1000)";
neuper@37906: val ct = "maximum A";
neuper@37906: val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
neuper@37906: 
neuper@37906: val ct = "valuesFor [a=Undef]";
neuper@37906: val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
neuper@37906: 
neuper@37906: val ct = "max_relation ()";
neuper@37906: val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
neuper@37906: 
neuper@37906: val ct = "relations [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]";
neuper@37906: val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
neuper@37906: 
neuper@37906: (* ... nxt = Specify_Domain ...
neuper@37906: val ct = "additionalRels [b=#2*R*cos alpha]";
neuper@37906: val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =
neuper@37906:    specify(Add_Relation ct) p c pt;
neuper@37906: (*
neuper@37906: val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
neuper@37906: *)
neuper@37906: val ct = "additionalRels [a=#2*R*sin alpha]";
neuper@37906: val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =
neuper@37906:    specify(Add_Relation ct) p c pt;
neuper@37906: (*
neuper@37906: val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
neuper@37906: *)
neuper@37906: *)
neuper@37906: (* --- tricky case (termlist interleaving variants):
neuper@37906: > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = 
neuper@37906:   specify (Init_Proof (cts,(dI,pI,mI))) [] [] EmptyPtree;
neuper@37906: 
neuper@37906: > val ct = "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2, b=#2*R*cos alpha]";
neuper@37906: > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
neuper@37906: *)
neuper@37906: 
neuper@37906: (* --- incomplete input ---
neuper@37906: > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = 
neuper@37906:   specify (Init_Proof (cts,(dI,pI,mI))) [] [] EmptyPtree;
neuper@37906: 
neuper@37906: > val ct = "[R=(R::real)]";
neuper@37906: > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
neuper@37906: 
neuper@37906: > val ct = "R=(R::real)";
neuper@37906: > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
neuper@37906: 
neuper@37906: > val ct = "(R::real)";
neuper@37906: > specify nxt p c pt;
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: " #################################################### ";
neuper@37906: "                   test  do_ specify                  ";
neuper@37906: " #################################################### ";
neuper@37906: 
neuper@37906: 
neuper@37906: val cts = ["fixedValues [R=(R::real)]", 
neuper@37906:            "boundVariable a", "boundVariable b",
neuper@37906:            "boundVariable alpha",
neuper@37906:            "domain {x::real. #0 <= x & x <= #2*R}",
neuper@37906: 	   "domain {x::real. #0 <= x & x <= #2*R}",
neuper@37906: 	   "domain {x::real. #0 <= x & x <= pi//#2}",
neuper@37906: 	   "errorBound (eps=#1//#1000)",
neuper@37906: 	   "maximum A","valuesFor [a=Undef]",
neuper@37906: 	 (*"functionTerm t","max_argument mx",      *)
neuper@37906: 	   "max_relation (A=#2*a*b - a^^^#2)",
neuper@37906: 	   "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", 
neuper@37906: 	   "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
neuper@37906: 	   "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"];
neuper@37906: val (dI',pI',mI')=
neuper@37991:   ("DiffAppl",["DiffAppl","test_maximum"],e_metID);
neuper@37906: val p = e_pos'; val c = []; 
neuper@37906: 
neuper@37906: val (mI,m) = ("Init_Proof",Init_Proof (cts, (dI',pI',mI')));
wneuper@59279: val (pst as (sc,pt,cl):pstate) = (EmptyScr, e_ctree, []);
neuper@37906: val (p,_,f,nxt,_,(_,pt,_)) = do_ (mI,m) p c pst;
neuper@37906: (*val nxt = ("Add_Given",Add_Given "fixedValues [R = R]")*)
neuper@37906: 
neuper@37906: val (p,_,Form' (PpcKF (_,_,ppc)),nxt,_,(_,pt,_)) = 
neuper@37906:   do_ nxt p c (EmptyScr,pt,[]);
neuper@37906: (*val nxt = ("Add_Given",Add_Given "boundVariable a") *)