neuper@37906: (*8.01: aufgehoben wegen alter preconds, postconds*)
neuper@37906: 
neuper@37906: (* rectangle with maximal area, inscribed in a circle of fixed radius
neuper@37906: 
neuper@37906: problem-types and methods solving the respective problem-type
neuper@37906: 
neuper@37906: (1) names of the problem-types and methods and their hierarchy
neuper@37906:     as subproblems.
neuper@37906:     names of problem-types are string lists (diss 5.3.), not shown
walther@59997:     here with exception of ["equation", "univariate"] in order to
neuper@37906:     indicate, that this particular problem needs refinement to a
neuper@37906:     more specific type of equation solvable by tan-square, etc.
neuper@37906: 
neuper@37906: problem-types                     methods
neuper@37906: -------------------------------   ----------------------
neuper@37906: maximum                           maximum-by-differentiation
neuper@37906:                                   maximum-by-experimentation
neuper@37906:   make-fun                        make-explicit-and-substitute 
neuper@37906:                                   introduce-a-new-variable
neuper@37906:   max-of-fun-on-interval          max-of-fun-on-interval
neuper@37906:     derivative                    differentiate
walther@59997:     ["equation", "univariate"]     tan-square
neuper@37906:                                   
neuper@37906:   find-values                     find-values
neuper@37906: 
neuper@37906: (2) specification of the problem-types
neuper@37906: *)
neuper@37906: 
neuper@37906: (* maximum *)
neuper@37906: (* ------- *)
neuper@37906: (* problem-type *)
neuper@37906: {given = ["fixed_values (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)"],
walther@59997:  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)))"],
walther@59997:  relate=["max_relation r", "additionalRels RS"]};
walther@60260: (*  \<up>  is exponenation *)
neuper@37906: 
neuper@37906: (* the functions Ex_frees, Rhs provide for the instantiation below *)
neuper@37906: 
neuper@37906: (* (1) instantiation of maximum, + variant in "values_for" *)
neuper@37906: {given = ["fixed_values (R = #7)"],
neuper@37906:  where_= ["is_equality (R = #7)",
neuper@37906: 	  "Not (R <= #0)"],
walther@59997:  find  =["maximum A", "values_for [a,b]"],
walther@60260:  with_ =["EX A. A = a*b & (a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2 \
walther@60260:   \ (ALL A'. A' = a*b & (a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2   \
neuper@37906:   \            --> A' <= A)))"],
neuper@37906:  relate=["max_relation (A = a*b)",
walther@60260: 	 "additionalRels [(a//#2) \<up> #2 +(b//#2) \<up> #2 =R \<up> #2]"]};
neuper@37906: (* R,a,b are bound by given, find *)
neuper@37906: 
neuper@37906: (* (2) instantiation of maximum *)
neuper@37906: {given = ["fixed_values (R = #7)"],
neuper@37906:  where_= ["is_equality (R = #7)",
neuper@37906: 	  "Not (R <= #0)"],
walther@59997:  find  =["maximum A", "values_for [A]"],
neuper@37906:  with_ =["EX a b alpha. A = a*b &                               \
neuper@37906:   \                     a = #2*R*sin alpha & b =#2*R*cos alpha &\
neuper@37906:   \ (ALL A'. A' = a*b & a = #2*R*sin alpha & b =#2*R*cos alpha  \
neuper@37906:   \            --> A' <= A)))"],
neuper@37906:  relate=["max_relation (A = a*b)",
wneuper@59377: 	 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]};
neuper@37906: (* R,A are bound by given, find *)
neuper@37906: 
neuper@37906: 
neuper@37906: (* make-fun *)
neuper@37906: (* -------- *)
neuper@37906: (* problem-type *)
walther@59997: {given = ["equality (lhs = rhs)", "bound_variable v", "equalities es"],
neuper@37906:  where_= [],
neuper@37906:  find  = ["function_term lhs_"],
neuper@37906:  with_ = [(*???*)],
neuper@37906:  relate= [(*???*)]};
neuper@37906: (*the _ in lhs is used to transfer the lhs-identifier of equality*)
neuper@37906: 
neuper@37906: (* (1) instantiation for make-explicit-and-substitute *)
walther@59997: {given = ["equality A = a * b", "bound_variable a", 
walther@60260: 	  "equalities [(a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2]"],
neuper@37906:  where_= [],
walther@60260:  find  = ["function_term A_"(*=(a * #2 * sqrt(R \<up> #2 - (a//#2) \<up> #2))*)],
neuper@37906:  with_ = [],
neuper@37906:  relate= []};
neuper@37906: 
neuper@37906: (* (2) instantiation for introduce-a-new-variable *)
walther@59997: {given = ["equality A = a * b", "bound_variable alpha", 
neuper@37906: 	  "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
neuper@37906:  where_= [],
neuper@37906:  find  = ["function_term A_"(*=(#2*R*sin alpha *#2*R*cos alpha)*)],
neuper@37906:  with_ = [],
neuper@37906:  relate= []};
neuper@37906: 
neuper@37906: 
neuper@37906: (* max-of-fun-on-interval *)
neuper@37906: (* ---------------------- *)
neuper@37906: (* problem-type *)
walther@59997: {given = ["function_term t", "bound_variable v",
neuper@37906: 	"domain {x::real. lower_bound <= x & x <= upper_bound}"],
neuper@37906:  where_= [],
neuper@37906:  find  = ["maximums ms"],
neuper@37906:  with_ = ["ALL m. m : ms --> \
neuper@37906:   \  (ALL x::real. lower_bound <= x & x <= upper_bound \
neuper@37906:   \        --> (%v. t) x <= m)"],
Walther@60586:  relate= []}: string model;
neuper@37906: (* ':' is 'element', '::' is a type constraint *)
neuper@37906: 
neuper@37906: (* (1) variant of instantiation *)
walther@60260: {given = ["function_term (a * #2 * sqrt(R \<up> #2 - (a//#2) \<up> #2))",
neuper@37906: 	"bound_variable a",
neuper@37906: 	"domain {x::real. #0 <= x & x <= #2*R}"],
neuper@37906:  where_= [],
neuper@37906:  find  = ["maximums AM"],
neuper@37906:  with_ = ["ALL am. am : AM --> \
neuper@37906:   \  (ALL x::real. #0 <= x & x <= #2*R \
walther@60260:   \        --> (%a. (a * #2 * sqrt(R \<up> #2 - (a//#2) \<up> #2))) x <= am)"],
neuper@37906:  relate= []};
neuper@37906: 
neuper@37906: (* (2) variant of instantiation *)
neuper@37906: {given = ["function_term (#2*R*sin alpha * #2*R*cos alpha)",
neuper@37906: 	"bound_variable alpha",
neuper@37906: 	"domain {x::real. #0 <= x & x <= pi//#2}"],
neuper@37906:  where_= [],
neuper@37906:  find  = ["maximums AM"],
neuper@37906:  with_ = ["ALL am. am : AM --> \
neuper@37906:   \  (ALL x::real. #0 <= x & x <= pi//#2 \
neuper@37906:   \        --> (%alpha. (#2*R*sin alpha * #2*R*cos alpha)) x <= am)"],
neuper@37906:  relate= []};
neuper@37906: 
neuper@37906: 
neuper@37906: (* derivative *)
neuper@37906: (* ---------- *)
neuper@37906: (* problem-type *)
walther@59997: {given = ["function_term t", "bound_variable bdv"],
neuper@37906:  where_= [],
neuper@37906:  find  = ["derivative t'"],
neuper@37906:  with_ = ["t' is_derivative_of (%bdv. t)"],
neuper@37906:  relate= []};
neuper@37906: (*the ' in t' is used to transfer the identifier from function_term*)
neuper@37906: 
neuper@37906: 
walther@59997: (* ["equation", "univariate"] *)
neuper@37906: (* ------------------------- *)
neuper@37906: (* problem-type *)
neuper@37906: {given = ["equality (lhs = rhs)",
walther@59997: 	  "bound_variable v", "error_bound eps"],
neuper@37906:  where_= [],
neuper@37906:  find  = ["solutions S"],
neuper@37906:  with_ = ["ALL s. s : S --> || (%v. lhs) s - (%v. rhs) s || <= eps"],
neuper@37906:  relate= []};
neuper@37906: 
neuper@37906: 
neuper@37906: (* find-values *)
neuper@37906: (* ----------- *)
neuper@37906: (* problem-type *)
walther@59997: {given = ["max_relation r", "additionalRels RS"],
neuper@37906:  where_= [],
neuper@37906:  find  = ["values_for VS"],
neuper@37906:  with_ = [(*???*)],
neuper@37906:  relate= []};
neuper@37906: 
neuper@37906: (* (1) variant of instantiation *)
neuper@37906: {given = ["max_relation (A = a*b)",
walther@60260: 	  "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2]"],
neuper@37906:  where_= [],
neuper@37906:  find  = ["values_for [a,b]"],
neuper@37906:  with_ = [],
neuper@37906:  relate= []};
neuper@37906: 
neuper@37906: (* (2) variant of instantiation *)
neuper@37906: {given = ["max_relation (A = a*b)",],
neuper@37906:  where_= [],
neuper@37906:  find  = ["values_for [A]",
wneuper@59377: 	  "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
neuper@37906:  with_ = [],
neuper@37906:  relate= []};
neuper@37906: 
neuper@37906: (*
neuper@37906: (3) data-transfer between the the hidden formalization, 
neuper@37906:     the root-problem and the sub-problems; 
neuper@37906: 
neuper@37906: maximum -> #given.make-fun
neuper@37906: -------------------
neuper@37906: maximum.#relate "max_relation r"         -> "equality (lhs = rhs)"
neuper@37906: formalization   "bound_variable v"       -> "bound_variable v"
wneuper@59377: maximum.#relate "additionalRels RS"-> "equalities es"
neuper@37906: 
neuper@37906: 
neuper@37906: maximum + make-fun -> #given.max-of-fun-on-interval
neuper@37906: --------------------------------------------
neuper@37906: make-fun.#find  "function_term lhs_"     -> "function_term t"
neuper@37906: make-fun.#given "bound_variable v"       -> "bound_variable v"
neuper@37906: formalization                            -> "domain {x::real. ...}"
neuper@37906: 
neuper@37906: 
neuper@37906: max-of-fun-on-interval -> #given.derivative
neuper@37906: ------------------------------------
neuper@37906: make-fun.#find  "function_term lhs_"     -> "function_term t"
neuper@37906: make-fun.#given "bound_variable v"       -> "bound_variable bdv"
neuper@37906: 
neuper@37906: 
neuper@37906: max-of-fun-on-interval + derivative -> 
walther@59997:                                 #given.["equation", "univariate"]
neuper@37906: ----------------------------------------------------------------
neuper@37906: derivative.#find "derivative t'"         -> "equality (lhs = rhs)"
neuper@37906:                                                       (* t'= #0 *)
neuper@37906: make-fun.#given  "bound_variable v"      -> "bound_variable v"
neuper@37906: formalization                            -> "error_bound eps"
neuper@37906: 
neuper@37906: 
neuper@37906: maximum + make-fun + max-of-fun-on-interval -> #given.find-values
neuper@37906: ----------------------------------------------------------
neuper@37906: maximum.#relate "max_relation r"         -> "max_relation r"
wneuper@59377: maximum.#relate "additionalRels RS"-> "additionalRels RS"
neuper@37906: *)
neuper@37906: 
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";
walther@60260:     \<up> --- geht nicht wegen fun-types *)
neuper@37906: 
neuper@37906: "pbltyp --- maximum ---";
neuper@37906: val pbltyp = {given=["fixed_values (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)"],
walther@59997: 	      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)))"],
Walther@60586: 	      relate=["max_relation r", "additionalRels rs"]}:string model;
walther@59989: val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
neuper@37906: "coil";
neuper@37906: val org = ["fixed_values [R=(R::real)]", 
neuper@37906: 	   "bound_variable a", "bound_variable b", "bound_variable 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: 	   "maximum A",
walther@60260: 	   "max_relation A=#2*a*b - a \<up> #2",
walther@60260: 	   "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2]", 
walther@60260: 	   "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2]", 
wneuper@59377: 	   "additionalRels [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=["fixed_values [R=(R::real)]"],where_=[],
walther@59997: 	   find=["maximum A", "values_for [a,b]"],
walther@60260: 	   with_=["EX alpha. A=#2*a*b - a \<up> #2 &    \
neuper@37906: 	    \ a=#2*R*sin alpha & b=#2*R*cos alpha & \
walther@60260: 	    \ (ALL A'. A'=#2*a*b - a \<up> #2 & a=#2*R*sin alpha & b=#2*R*cos alpha \
neuper@37906: 	    \         --> A' <= A)"],
walther@60260: 	   relate=["max_relation (A=#2*a*b - a \<up> #2)",
wneuper@59377: 		   "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
Walther@60586: 	  }: string model;
walther@59989: val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
neuper@37906: 
neuper@37906: "met --- maximum_by_differentiation ---";
walther@59997: val met = {given=["fixed_values (cs::bool list)", "bound_variable v",
neuper@37906: 		  "domain {x::real. lower_bound <= x & x <= upper_bound}",
neuper@37906: 		  "approximation apx"],
neuper@37906: 	   where_=[],
walther@59997: 	   find=["maximum m", "values_for (ms::real list)",
walther@59997: 		 "function_term t", "max_argument mx"],
neuper@37906: 	   with_=["Ex_frees ((foldl (op &) True (rs::bool list)) & \
neuper@37906:                   \ (ALL m'. (subst (m,m') (foldl (op &) True rs)  \
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)"],
Walther@60586: 	   relate=["rs::bool list"]}: string model;
walther@59989: val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) met;
neuper@37906: 
neuper@37906: 
neuper@37906: "pbltyp --- make_fun ---";
neuper@37906: (* subproblem [(hd #relate root, equality),
neuper@37906:                (bound_variable formalization, bound_variable),
neuper@37906: 	       (tl #relate root, equalities)] *) 
walther@59997: val pbltyp = {given=["equality e", "bound_variable v", "equalities es"],
neuper@37906: 	      where_=[],
neuper@37906: 	      find=["function_term t"],with_=[(*???*)],
Walther@60586: 	      relate=[(*???*)]}: string model;
walther@59989: val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
neuper@37906: "coil";
walther@60260: val pbl = {given=["equality (A=#2*a*b - a \<up> #2)", "bound_variable alpha",
neuper@37906: 		  "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
neuper@37906: 	   where_=[],
neuper@37906: 	   find=["function_term t"],
Walther@60586: 	   with_=[],relate=[]}: string model;
walther@59989: val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
neuper@37906: 
neuper@37906: "met --- make_explicit_and_substitute ---";
walther@59997: val met = {given=["equality e", "bound_variable v", "equalities es"],
neuper@37906: 	   where_=[],
neuper@37906: 	   find=["function_term t"],with_=[(*???*)],
Walther@60586: 	   relate=[(*???*)]}: string model;
walther@59989: val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met;
neuper@37906: "met --- introduce_a_new_variable ---";
walther@59997: val met = {given=["equality e", "bound_variable v", "substitutions es"],
neuper@37906: 	   where_=[],
neuper@37906: 	   find=["function_term t"],with_=[(*???*)],
Walther@60586: 	   relate=[(*???*)]}: string model;
walther@59989: val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met;
neuper@37906: 
neuper@37906: 
neuper@37906: "pbltyp --- max_of_fun_on_interval ---";
walther@59997: val pbltyp = {given=["function_term t", "bound_variable v",
neuper@37906: 		     "domain {x::real. lower_bound <= x & x <= upper_bound}"],
neuper@37906: 	      where_=[],
neuper@37906: 	      find=["maximums ms"],
neuper@37906: 	      with_=["ALL m. m : ms --> \
neuper@37906: 	             \  (ALL x::real. lower_bound <= x & x <= upper_bound \
neuper@37906: 	             \        --> (%v. t) x <= m)"],
Walther@60586: 	      relate=[]}: string model;
walther@59989: val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
neuper@37906: "coil";
neuper@37906: val pbl = {given=["function_term #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \
walther@60260:                    \ (#2*R*sin alpha) \<up> #2", "bound_variable alpha",
neuper@37906: 		  "domain {x::real. #0 <= x & x <= pi}"],where_=[],
Walther@60586: 	   find=["maximums [#1234]"],with_=[],relate=[]}: string model;
walther@59989: val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
neuper@37906: 
neuper@37906: 
neuper@37906: (* pbltyp --- max_of_fun --- *)
neuper@37906: (*
Walther@60586: {given=[],where_=[],find=[],with_=[],relate=[]}: string model;
neuper@37926: val (SOME ct) = parse thy ;
Walther@60650: TermC.atom_trace_detail @{context} (Thm.term_of ct);
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (* --- 14.1.00 --- *)
neuper@37906: "p.114";
neuper@37906: val org = {given=["[u=(#12::real)]"],where_=[],
neuper@37906: 	   find=["[a,(b::real)]"],with_=[],
Walther@60586: 	   relate=["[is_max A=a*(b::real), #2*a+#2*b=(u::real)]"]}: string model;
walther@59989: val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
neuper@37906: "p.116";
neuper@37906: val org = {given=["[c=#10, h=(#4::real)]"],where_=[],
neuper@37906: 	   find=["[x,(y::real)]"],with_=[],
Walther@60586: 	   relate=["[A=x*(y::real), c//h=x//(h-(y::real))]"]}: string model;
walther@59989: val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
neuper@37906: "p.117";
neuper@37906: val org = {given=["[r=#5]"],where_=[],
neuper@37906: 	   find=["[x,(y::real)]"],with_=[],
Walther@60586: 	   relate=["[is_max #0=pi*x \<up> #2 + pi*x*(r::real)]"]}: string model;
walther@59989: val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
neuper@37906: "#241";
neuper@37906: val org = {given=["[s=(#10::real)]"],where_=[],
neuper@37906: 	   find=["[p::real]"],with_=[],
Walther@60586: 	   relate=["[is_max p=n*m, s=n+(m::real)]"]}: string model;
walther@59989: val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
neuper@37906: 
neuper@37906: (*
Walther@60586: {given=[],where_=[],find=[],with_=[],relate=[]}: string model;
neuper@37926: val (SOME ct) = parse thy ;
Walther@60650: TermC.atom_trace_detail @{context} (Thm.term_of ct);
neuper@37906: *)