diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/IsacKnowledge/DiffApp-oldpbl.sml --- a/src/Tools/isac/IsacKnowledge/DiffApp-oldpbl.sml Wed Aug 25 15:15:01 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,369 +0,0 @@ -(*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","additional_relations RS"]}; -(* ^^^ 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)^^^#2 + (b//#2)^^^#2 = R^^^#2 \ - \ (ALL A'. A' = a*b & (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2 \ - \ --> A' <= A)))"], - relate=["max_relation (A = a*b)", - "additional_relations [(a//#2)^^^#2 +(b//#2)^^^#2 =R^^^#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)", - "additional_relations [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)^^^#2 + (b//#2)^^^#2 = R^^^#2]"], - where_= [], - find = ["function_term A_"(*=(a * #2 * sqrt(R^^^#2 - (a//#2)^^^#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 ppc; -(* ':' is 'element', '::' is a type constraint *) - -(* (1) variant of instantiation *) -{given = ["function_term (a * #2 * sqrt(R^^^#2 - (a//#2)^^^#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^^^#2 - (a//#2)^^^#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","additional_relations RS"], - where_= [], - find = ["values_for VS"], - with_ = [(*???*)], - relate= []}; - -(* (1) variant of instantiation *) -{given = ["max_relation (A = a*b)", - "additional_relations [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]"], - where_= [], - find = ["values_for [a,b]"], - with_ = [], - relate= []}; - -(* (2) variant of instantiation *) -{given = ["max_relation (A = a*b)",], - where_= [], - find = ["values_for [A]", - "additional_relations [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 "additional_relations 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 "additional_relations RS"-> "additional_relations 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"; - ^^^--- 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","additional_relations rs"]}:string ppc; -val chkpbltyp = ((map (the o (parse thy))) o ppc2list) 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^^^#2", - "additional_relations [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]", - "additional_relations [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]", - "additional_relations [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^^^#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=["max_relation (A=#2*a*b - a^^^#2)", - "additional_relations [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=["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 ppc; -val chkpbl = ((map (the o (parse thy))) o ppc2list) 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 ppc; -val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp; -"coil"; -val pbl = {given=["equality (A=#2*a*b - a^^^#2)","bound_variable alpha", - "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"], - where_=[], - find=["function_term 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","bound_variable v", "equalities es"], - where_=[], - find=["function_term 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","bound_variable v", "substitutions es"], - where_=[], - find=["function_term t"],with_=[(*???*)], - relate=[(*???*)]}: string ppc; -val chkmet = ((map (the o (parse thy))) o ppc2list) 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 ppc; -val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp; -"coil"; -val pbl = {given=["function_term #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \ - \ (#2*R*sin alpha)^^^#2","bound_variable 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 thy (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 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; - -(* -{given=[],where_=[],find=[],with_=[],relate=[]}: string ppc; -val (SOME ct) = parse thy ; -atomty thy (term_of ct); -*)