(* use"test-coil-kernel.sml";

   W.N.22.11.99

*)

(* vvv--- geht nicht wegen fun-types

parse thy "case maxmin of is_max => (m' <= m) | is_min => (m <= m')";

parse thy "if maxmin = is_max then (m' <= m) else (m <= m')";

parse thy "if a=b then a else b";

parse thy "maxmin = is_max";

parse thy "maxmin =!= is_max";

   ^^^--- geht nicht wegen fun-types *)

"pbltyp --- maximum ---";

val pbltyp = {given=["fixedValues (cs::bool list)"],

	      where_=[(*"foldl (op &) True (map is_equality cs)",

		      "foldl (op &) True (map (Not o ((op <=) #0) o Rhs) cs)"*)],

	      find=["maximum m","values_for (ms::real list)"],

	      with_=[(*"Ex_frees ((foldl (op &) True (r#rs)) &              \

                      \ (ALL m'. (subst (m,m') (foldl (op &) True (r#rs)) \

		      \            --> m' <= m)))"*)],

	      relate=["max_relation r","additionalRels rs"]}:string ppc;

val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;

"coil";

val org = ["fixedValues [R=(R::real)]", 

	   "boundVariable a","boundVariable b","boundVariable alpha",

	   "domain {x::real. #0 <= x & x <= #2*R}",

	   "domain {x::real. #0 <= x & x <= #2*R}",

	   "domain {x::real. #0 <= x & x <= pi}",

	   "errorBound (eps = #1//#1000)",

	   "maximum A",

	 (*"max_relation A=#2*a*b - a^^^#2",*)

	   "relations [A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",

	   "relations [A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",

	   "relations [A=#2*a*b - a^^^#2, a=#2*R*sin alpha, b=#2*R*cos alpha]"];

val chkorg = map (the o (parse thy)) org;

val pbl = {given=["fixedValues [R=(R::real)]"],where_=[],

	   find=["maximum A","values_for [a,b]"],

	   with_=[(* incompat.w. parse, ok with parseold

		   "EX alpha. A=#2*a*b - a^^^#2 &    \

	    \ a=#2*R*sin alpha & b=#2*R*cos alpha & \

	    \ (ALL A'. A'=#2*a*b - a^^^#2 & a=#2*R*sin alpha \

	    \          & b=#2*R*cos alpha \

	    \         --> A' <= A)"*)],

	   relate=["relations [A=#2*a*b - a^^^#2, a=#2*R*sin alpha, b=#2*R*cos alpha]"]

	  }: string ppc;

val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;

"met --- maximum_by_differentiation ---";

val met = {given=["fixedValues (cs::bool list)","boundVariable v",

		  "domain {x::real. lower_bound <= x & x<=upper_bound}",

		  "errorBound epsilon"],

	   where_=[],

	   find=["maximum m","valuesFor (ms::bool list)",

		 "function_term t","max_argument mx"],

	   with_=[(* incompat.w. parse, ok with parseold

		   "Ex_frees ((foldl (op &) True (mr#ars)) &           \

                  \ (ALL m'. (subst (m,m') (foldl (op &) True (mr#ars))\

		  \            --> m' <= m))) &                        \

		  \m = (%v. t) mx &                                    \

                  \( ALL x. lower_bound <= x & x <= upper_bound        \

	          \       --> (%v. t) x <= m)"*)],

	   relate=["max_relation mr",

		   "additionalRels ars"]}: string ppc;

val chkpbl = ((map (the o (parse thy))) o ppc2list) met;

"data --- maximum_by_differentiation ---";

val met = {given=["fixedValues [R=(R::real)]","boundVariable alpha",

		  "domain {x::real. #0 <= x & x <= pi//#2}",

		  "errorBound (eps = #1//#1000)"],

	   where_=[],

	   find=["maximum A","valuesFor [a=Undef]",

		 "function_term t","max_argument mx"],

	   with_=[(* incompat.w. parse, ok with parseold

		   "EX b alpha. A = #2*a*b - a^^^#2 &     \

	            \          a = #2*R*sin alpha  &     \

		    \          b = #2*R*cos alpha  &     \

		    \ (ALL A'. A'= #2*a*b - a^^^#2 &     \

	            \          a = #2*R*sin alpha  &     \

		    \          b = #2*R*cos alpha  --> A' <= A) & \

		    \ A = (%alpha. t) mx &               \

		    \ (ALL x. #0 <= x & x <= pi -->      \

                    \          (%alpha. t) x <= A)"*)],

	   relate=["max_relation mr",

		   "additionalRels ars"]}: string ppc;

val chkpbl = ((map (the o (parse thy))) o ppc2list) met;

val (SOME ct) = parseold thy "EX b. (EX alpha. A = #2*a*b - a^^^#2)";

"pbltyp --- make_fun ---";

(* subproblem [(hd #relate root, equality),

               (boundVariable formalization, boundVariable),

	       (tl #relate root, equalities)] *) 

val pbltyp = {given=["equality e","boundVariable v", "equalities es"],

	      where_=[],

	      find=["functionTerm t"],with_=[(*???*)],

	      relate=[(*???*)]}: string ppc;

val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;

"coil";

val pbl = {given=["equality (A=#2*a*b - a^^^#2)","boundVariable alpha",

		  "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],

	   where_=[],

	   find=["functionTerm t"],

	   with_=[],relate=[]}: string ppc;

val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;

"met --- make_explicit_and_substitute ---";

val met = {given=["equality e","boundVariable v", "equalities es"],

	   where_=[],

	   find=["functionTerm t"],with_=[(*???*)],

	   relate=[(*???*)]}: string ppc;

val chkmet = ((map (the o (parse thy))) o ppc2list) met;

"met --- introduce_a_new_variable ---";

val met = {given=["equality e","boundVariable v", "substitutions es"],

	   where_=[],

	   find=["functionTerm t"],with_=[(*???*)],

	   relate=[(*???*)]}: string ppc;

val chkmet = ((map (the o (parse thy))) o ppc2list) met;

"pbltyp --- max_of_fun_on_interval ---";

val pbltyp = {given=["functionTerm t","boundVariable v",

		     "domain {x::real. lower_bound <= x & x <= upper_bound}"],

	      where_=[],

	      find=["maximums ms"],

	      with_=[(* incompat.w. parse, ok with parseold

		   "ALL m. m : ms --> \

	          \  (ALL x::real. lower_bound <= x & x <= upper_bound \

	          \        --> (%v. t) x <= m)"*)],

	      relate=[]}: string ppc;

val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;

"coil";

val pbl = {given=["functionTerm (f = #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \

                   \ (#2*R*sin alpha)^^^#2)","boundVariable alpha",

		  "domain {x::real. #0 <= x & x <= pi}"],where_=[],

	   find=["maximums [#1234]"],with_=[],relate=[]}: string ppc;

val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;

(* pbltyp --- max_of_fun --- *)

(*

{given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;

val (SOME ct) = parse thy ;

atomty (Thm.term_of ct);

*)

(* --- 14.1.00 ev. nicht ganz up to date bzg. oberem --- *)

"p.114";

val org = {given=["[u=(#12::real)]"],where_=[],

	   find=["[a,(b::real)]"],with_=[],

	   relate=["[is_max A=a*(b::real), #2*a+#2*b=(u::real)]"]}: string ppc;

val chkorg = ((map (the o (parse thy))) o ppc2list) org;

"p.116";

val org = {given=["[c=#10, h=(#4::real)]"],where_=[],

	   find=["[x,(y::real)]"],with_=[],

	   relate=["[A=x*(y::real), c//h=x//(h-(y::real))]"]}: string ppc;

val chkorg = ((map (the o (parse thy))) o ppc2list) org;

"p.117";

val org = {given=["[r=#5]"],where_=[],

	   find=["[x,(y::real)]"],with_=[],

	   relate=["[is_max #0=pi*x^^^#2 + pi*x*(r::real)]"]}: string ppc;

val chkorg = ((map (the o (parse thy))) o ppc2list) org;

"#241";

val org = {given=["[s=(#10::real)]"],where_=[],

	   find=["[p::real]"],with_=[],

	   relate=["[is_max p=n*m, s=n+(m::real)]"]}: string ppc;

val chkorg = ((map (the o (parse thy))) o ppc2list) org;

(* -------------- coil-kernel -------------- vor 19.1.00 *)

(* --- subproblem: make-function-by-subst    ~~~~~~~~~~~ *)

(* --- subproblem: max-of-function *)

(* --- subproblem: derivative *)

(* --- subproblem: tan-quadrat-equation *)

"-------------- coil-kernel --------------";

val origin = ["A=#2*a*b - a^^^#2",

	      "a::real","b::real","{x. #0<x & x<R//#2}",

	      "{(a//#2)^^^#2 + (b//#2)^^^#2 = (R//#2)^^^#2}",

	      "alpha::real","{alpha::real. #0<alpha & alpha<pi//#2}",

	      "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",

	      "{R::real}"];

(* --- for a isa-users-mail --- FIXME

Goal "{x. x < a} = ?z";

{x::'a. x < a} = ?z

Goal "{x. x < #3} = {a}";

{x::'a. x < (#3::'a)} = {a}

Goal "{x. #3 < x} = ?z";

Collect (op < (#3::'a)) = ?z

---------------------------- *)

val formals = map (the o (parse thy)) origin;

val given  = ["formula_for_max (lhs=rhs)","boundVariable bdv",

	      "interval {x. low < x & x < high}",

	      "additional_conds ac","constants cs"];

val where_ = ["lhs is_const","bdv is_const","low is_const","high is_const",

	      "||| Vars equ ||| = ||| VarsSet ac ||| - ||| ac ||| + #1"];

val find   = ["f::real => real","maxs::real set"];

val with_  = [(* incompat.w. parse, ok with parseold

		   "maxs = {m. low < m & m < high & \

                        \ (m is_local_max_of (%bdv. f))}"*)];

val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);

val givens = map (the o (parse thy)) given;

"------- 1.1 -------";

(* 5.3.00

val formals = map (the o (parse thy)) ["A=#2*a*b - a^^^#2",

	      "a::real","{x. #0<x & x<R//#2}",

	      "{(a//#2)^^^#2 + (b//#2)^^^#2 = (R//#2)^^^#2}",

	      "{R::real}"];

val tag__forms = chktyps thy (formals, givens);

map ((atomty) o Thm.term_of) tag__forms;

val formals = map (the o (parse thy)) ["A=#2*a*b - a^^^#2",

	      "alpha::real","{alpha. #0<alpha & alpha<pi//#2}",

	      "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",

	      "{R::real}"];

val tag__forms = chktyps thy (formals, givens);

map ((atomty) o Thm.term_of) tag__forms;

*)

" --- subproblem: make-function-by-subst --- ";

val origin = ["A=#2*a*b - a^^^#2",

	      "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",

	      "{R::real}"];

val formals = map (the o (parse thy)) origin;

val given  = ["equation (lhs=rhs)","substitutions ss",

	      "constants cs"];

val where_ = [];

val find   = ["t::real"];

val with_  = ["||| Vars t ||| = #1"];

val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);

val givens = map (the o (parse thy)) given;

(* 5.3.00

val tag__forms = chktyps thy (formals, givens);

map ((atomty) o Thm.term_of) tag__forms;

*)

" --- subproblem: max-of-function --- ";

val origin = ["A = #2*(#2*R*(sin alpha))*(#2*R*(sin alpha)) - \

               \ (#2*R*(sin alpha))^^^#2",

	      "{alpha. #0<alpha & alpha<pi//#2}",

	      "{R::real}"];

val formals = map (the o (parse thy)) origin;

val given  = ["equation (lhs=rhs)",

	      "interval {x. low < x & x < high}",

	      "constants cs"];

val where_ = ["lhs is_const","low is_const","high is_const"];

val find   = ["t::real"];

val with_  = ["||| Vars t ||| = #1"];

val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);

val givens = map (the o (parse thy)) given;

(* 5.3.00

val tag__forms = chktyps thy (formals, givens);

map ((atomty) o Thm.term_of) tag__forms;

*)

" --- subproblem: derivative --- ";

val origin = ["x^^^#3-y^^^#3+#-3*x+#12*y+#10","x::real"];

val formals = map (the o (parse thy)) origin;

val given  = ["functionTerm t",

	      "boundVariable bdv"];

val where_ = ["bdv is_const"];

val find   = ["t'::real"];

val with_  = ["t' is_derivative_of (%bdv. t)"];

val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);

val givens = map (the o (parse thy)) given;

(*

val tag__forms = chktyps thy (formals, givens);

map ((atomty) o Thm.term_of) tag__forms;

*)

" --- subproblem: tan-quadrat-equation --- ";

val origin = ["#8*R^^^#2*(cos alpha)^^^#2 + #-8*R^^^#2* \

	      \ (cos alpha)*(sin alpha) + #8*R^^^#2*(sin alpha)^^^#2 = #0",

	      "alpha::real","#1//#1000"];

val formals = map (the o (parse thy)) origin;

val given  = ["equation (a*(cos bdv)^^^#2 + b*(cos bdv)*(sin bdv) + \

	      \ c*(sin bdv) = #0)",

	     "boundVariable bdv","errorBound epsilon"];

val where_ = ["bdv is_const","epsilon is_const_expr"];

val find   = ["L::real set"];

val with_  = ["L = {x. || (%bdv. a*(cos bdv)^^^#2 + b*(cos bdv)*(sin bdv) + \

	      \ c*(sin bdv)) x || < epsilon}"];

(* 5.3.00

val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);

val givens = map (the o (parse thy)) given;

val tag__forms = chktyps thy (formals, givens);

map ((atomty) o Thm.term_of) tag__forms;

*)

(*  use"test-coil-kernel.sml";

  *)

" #################################################### ";

"                       test specify                   ";

" #################################################### ";

val cts = 

["fixedValues [R=(R::real)]", 

 "boundVariable a", "boundVariable b",

 "boundVariable alpha",

 "domain {x::real. #0 <= x & x <= #2*R}",

 "domain {x::real. #0 <= x & x <= #2*R}",

 "domain {x::real. #0 <= x & x <= pi//#2}",

 "errorBound (eps = #1//#1000)",

 "maximum A","valuesFor [a=Undef]",

 (*"functionTerm t","max_argument mx", 

  "max_relation (A=#2*a*b - a^^^#2)",      *)

 "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", 

 "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",

 "additionalRels [A=#2*a*b - a^^^#2,a=#2*R*sin alpha, b=#2*R*cos alpha]"];

val (dI',pI',mI')=

  ("DiffAppl",["Script","maximum_of","function"],e_metID);

val c = []:cid;

(*

val pbl = {given=["fixedValues [R=(R::real)]","boundVariable alpha",

		  "domain {x::real. #0 <= x & x <= pi//#2}",

		  "errorBound (eps = #1//#1000)"],

	   where_=[],

	   find=["maximum A","valuesFor [a=Undef]"(*,

		 "functionTerm t","max_argument mx"*)],

	   with_=[],

	   relate=["max_relation (A=#2*a*b - a^^^#2)",

	   "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", 

	   "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",

	   "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]

	   }: string ppc;

*)

val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = 

  specify (Init_Proof (cts,(dI',pI',mI'))) e_pos' [] EmptyPtree;

val ct = "fixedValues [R=(R::real)]";

(*l(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify(Add_Given ct) p c pt*)

val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;

val ct = "boundVariable a";

val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;

val ct = "boundVariable alpha";

val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;

val ct = "domain {x::real. #0 <= x & x <= pi//#2}";

val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;

val ct = "errorBound (eps = (#1::real) // #1000)";

val ct = "maximum A";

val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;

val ct = "valuesFor [a=Undef]";

val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;

val ct = "max_relation ()";

val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;

val ct = "relations [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]";

val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;

(* ... nxt = Specify_Domain ...

val ct = "additionalRels [b=#2*R*cos alpha]";

val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =

   specify(Add_Relation ct) p c pt;

(*

val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;

*)

val ct = "additionalRels [a=#2*R*sin alpha]";

val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =

   specify(Add_Relation ct) p c pt;

(*

val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;

*)

*)

(* --- tricky case (termlist interleaving variants):

> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = 

  specify (Init_Proof (cts,(dI,pI,mI))) [] [] EmptyPtree;

> val ct = "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2, b=#2*R*cos alpha]";

> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;

*)

(* --- incomplete input ---

> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = 

  specify (Init_Proof (cts,(dI,pI,mI))) [] [] EmptyPtree;

> val ct = "[R=(R::real)]";

> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;

> val ct = "R=(R::real)";

> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;

> val ct = "(R::real)";

> specify nxt p c pt;

*)

" #################################################### ";

"                   test  do_ specify                  ";

" #################################################### ";

val cts = ["fixedValues [R=(R::real)]", 

           "boundVariable a", "boundVariable b",

           "boundVariable alpha",

           "domain {x::real. #0 <= x & x <= #2*R}",

	   "domain {x::real. #0 <= x & x <= #2*R}",

	   "domain {x::real. #0 <= x & x <= pi//#2}",

	   "errorBound (eps=#1//#1000)",

	   "maximum A","valuesFor [a=Undef]",

	 (*"functionTerm t","max_argument mx",      *)

	   "max_relation (A=#2*a*b - a^^^#2)",

	   "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", 

	   "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",

	   "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"];

val (dI',pI',mI')=

  ("DiffAppl",["DiffAppl","test_maximum"],e_metID);

val p = e_pos'; val c = []; 

val (mI,m) = ("Init_Proof",Init_Proof (cts, (dI',pI',mI')));

val (pst as (sc,pt,cl):pstate) = (EmptyScr, e_ctree, []);

val (p,_,f,nxt,_,(_,pt,_)) = do_ (mI,m) p c pst;

(*val nxt = ("Add_Given",Add_Given "fixedValues [R = R]")*)

val (p,_,Form' (PpcKF (_,_,ppc)),nxt,_,(_,pt,_)) = 

  do_ nxt p c (EmptyScr,pt,[]);

(*val nxt = ("Add_Given",Add_Given "boundVariable a") *)