(*8.01: aufgehoben wegen alter preconds, postconds*)

(* rectangle with maximal area, inscribed in a circle of fixed radius

problem-types and methods solving the respective problem-type

(1) names of the problem-types and methods and their hierarchy

    as subproblems.

    names of problem-types are string lists (diss 5.3.), not shown

    here with exception of ["equation", "univariate"] in order to

    indicate, that this particular problem needs refinement to a

    more specific type of equation solvable by tan-square, etc.

problem-types                     methods

-------------------------------   ----------------------

maximum                           maximum-by-differentiation

                                  maximum-by-experimentation

  make-fun                        make-explicit-and-substitute 

                                  introduce-a-new-variable

  max-of-fun-on-interval          max-of-fun-on-interval

    derivative                    differentiate

    ["equation", "univariate"]     tan-square

  find-values                     find-values

(2) specification of the problem-types

*)

(* maximum *)

(* ------- *)

(* problem-type *)

{given = ["fixed_values (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"]};

(*  \<up>  is exponenation *)

(* the functions Ex_frees, Rhs provide for the instantiation below *)

(* (1) instantiation of maximum, + variant in "values_for" *)

{given = ["fixed_values (R = #7)"],

 where_= ["is_equality (R = #7)",

	  "Not (R <= #0)"],

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

 with_ =["EX A. A = a*b & (a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2 \

  \ (ALL A'. A' = a*b & (a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2   \

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

 relate=["max_relation (A = a*b)",

	 "additionalRels [(a//#2) \<up> #2 +(b//#2) \<up> #2 =R \<up> #2]"]};

(* R,a,b are bound by given, find *)

(* (2) instantiation of maximum *)

{given = ["fixed_values (R = #7)"],

 where_= ["is_equality (R = #7)",

	  "Not (R <= #0)"],

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

 with_ =["EX a b alpha. A = a*b &                               \

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

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

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

 relate=["max_relation (A = a*b)",

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

(* R,A are bound by given, find *)

(* make-fun *)

(* -------- *)

(* problem-type *)

{given = ["equality (lhs = rhs)", "bound_variable v", "equalities es"],

 where_= [],

 find  = ["function_term lhs_"],

 with_ = [(*???*)],

 relate= [(*???*)]};

(*the _ in lhs is used to transfer the lhs-identifier of equality*)

(* (1) instantiation for make-explicit-and-substitute *)

{given = ["equality A = a * b", "bound_variable a", 

	  "equalities [(a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2]"],

 where_= [],

 find  = ["function_term A_"(*=(a * #2 * sqrt(R \<up> #2 - (a//#2) \<up> #2))*)],

 with_ = [],

 relate= []};

(* (2) instantiation for introduce-a-new-variable *)

{given = ["equality A = a * b", "bound_variable alpha", 

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

 where_= [],

 find  = ["function_term A_"(*=(#2*R*sin alpha *#2*R*cos alpha)*)],

 with_ = [],

 relate= []};

(* max-of-fun-on-interval *)

(* ---------------------- *)

(* problem-type *)

{given = ["function_term t", "bound_variable v",

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

 where_= [],

 find  = ["maximums ms"],

 with_ = ["ALL m. m : ms --> \

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

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

 relate= []}: string model;

(* ':' is 'element', '::' is a type constraint *)

(* (1) variant of instantiation *)

{given = ["function_term (a * #2 * sqrt(R \<up> #2 - (a//#2) \<up> #2))",

	"bound_variable a",

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

 where_= [],

 find  = ["maximums AM"],

 with_ = ["ALL am. am : AM --> \

  \  (ALL x::real. #0 <= x & x <= #2*R \

  \        --> (%a. (a * #2 * sqrt(R \<up> #2 - (a//#2) \<up> #2))) x <= am)"],

 relate= []};

(* (2) variant of instantiation *)

{given = ["function_term (#2*R*sin alpha * #2*R*cos alpha)",

	"bound_variable alpha",

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

 where_= [],

 find  = ["maximums AM"],

 with_ = ["ALL am. am : AM --> \

  \  (ALL x::real. #0 <= x & x <= pi//#2 \

  \        --> (%alpha. (#2*R*sin alpha * #2*R*cos alpha)) x <= am)"],

 relate= []};

(* derivative *)

(* ---------- *)

(* problem-type *)

{given = ["function_term t", "bound_variable bdv"],

 where_= [],

 find  = ["derivative t'"],

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

 relate= []};

(*the ' in t' is used to transfer the identifier from function_term*)

(* ["equation", "univariate"] *)

(* ------------------------- *)

(* problem-type *)

{given = ["equality (lhs = rhs)",

	  "bound_variable v", "error_bound eps"],

 where_= [],

 find  = ["solutions S"],

 with_ = ["ALL s. s : S --> || (%v. lhs) s - (%v. rhs) s || <= eps"],

 relate= []};

(* find-values *)

(* ----------- *)

(* problem-type *)

{given = ["max_relation r", "additionalRels RS"],

 where_= [],

 find  = ["values_for VS"],

 with_ = [(*???*)],

 relate= []};

(* (1) variant of instantiation *)

{given = ["max_relation (A = a*b)",

	  "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2]"],

 where_= [],

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

 with_ = [],

 relate= []};

(* (2) variant of instantiation *)

{given = ["max_relation (A = a*b)",],

 where_= [],

 find  = ["values_for [A]",

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

 with_ = [],

 relate= []};

(*

(3) data-transfer between the the hidden formalization, 

    the root-problem and the sub-problems; 

maximum -> #given.make-fun

-------------------

maximum.#relate "max_relation r"         -> "equality (lhs = rhs)"

formalization   "bound_variable v"       -> "bound_variable v"

maximum.#relate "additionalRels RS"-> "equalities es"

maximum + make-fun -> #given.max-of-fun-on-interval

--------------------------------------------

make-fun.#find  "function_term lhs_"     -> "function_term t"

make-fun.#given "bound_variable v"       -> "bound_variable v"

formalization                            -> "domain {x::real. ...}"

max-of-fun-on-interval -> #given.derivative

------------------------------------

make-fun.#find  "function_term lhs_"     -> "function_term t"

make-fun.#given "bound_variable v"       -> "bound_variable bdv"

max-of-fun-on-interval + derivative -> 

                                #given.["equation", "univariate"]

----------------------------------------------------------------

derivative.#find "derivative t'"         -> "equality (lhs = rhs)"

                                                      (* t'= #0 *)

make-fun.#given  "bound_variable v"      -> "bound_variable v"

formalization                            -> "error_bound eps"

maximum + make-fun + max-of-fun-on-interval -> #given.find-values

----------------------------------------------------------

maximum.#relate "max_relation r"         -> "max_relation r"

maximum.#relate "additionalRels RS"-> "additionalRels RS"

*)

(* 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";

    \<up> --- geht nicht wegen fun-types *)

"pbltyp --- maximum ---";

val pbltyp = {given=["fixed_values (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 model;

val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;

"coil";

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

	   "bound_variable a", "bound_variable b", "bound_variable alpha",

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

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

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

	   "maximum A",

	   "max_relation A=#2*a*b - a \<up> #2",

	   "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2]", 

	   "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2]", 

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

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

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

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

	   with_=["EX alpha. A=#2*a*b - a \<up> #2 &    \

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

	    \ (ALL A'. A'=#2*a*b - a \<up> #2 & a=#2*R*sin alpha & b=#2*R*cos alpha \

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

	   relate=["max_relation (A=#2*a*b - a \<up> #2)",

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

	  }: string model;

val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;

"met --- maximum_by_differentiation ---";

val met = {given=["fixed_values (cs::bool list)", "bound_variable v",

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

		  "approximation apx"],

	   where_=[],

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

		 "function_term t", "max_argument mx"],

	   with_=["Ex_frees ((foldl (op &) True (rs::bool list)) & \

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

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

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

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

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

	   relate=["rs::bool list"]}: string model;

val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) met;

"pbltyp --- make_fun ---";

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

               (bound_variable formalization, bound_variable),

	       (tl #relate root, equalities)] *) 

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

	      where_=[],

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

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

val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;

"coil";

val pbl = {given=["equality (A=#2*a*b - a \<up> #2)", "bound_variable alpha",

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

	   where_=[],

	   find=["function_term t"],

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

val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;

"met --- make_explicit_and_substitute ---";

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

	   where_=[],

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

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

val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met;

"met --- introduce_a_new_variable ---";

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

	   where_=[],

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

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

val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met;

"pbltyp --- max_of_fun_on_interval ---";

val pbltyp = {given=["function_term t", "bound_variable v",

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

	      where_=[],

	      find=["maximums ms"],

	      with_=["ALL m. m : ms --> \

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

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

	      relate=[]}: string model;

val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;

"coil";

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

                   \ (#2*R*sin alpha) \<up> #2", "bound_variable alpha",

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

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

val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;

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

(*

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

val (SOME ct) = parse thy ;

TermC.atom_trace_detail @{context} (Thm.term_of ct);

*)

(* --- 14.1.00 --- *)

"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 model;

val chkorg = ((map (the o (parse thy))) o P_Model.to_list) 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 model;

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

"p.117";

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

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

	   relate=["[is_max #0=pi*x \<up> #2 + pi*x*(r::real)]"]}: string model;

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

"#241";

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

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

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

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

(*

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

val (SOME ct) = parse thy ;

TermC.atom_trace_detail @{context} (Thm.term_of ct);

*)