1.1 --- a/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml Tue May 19 12:33:35 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml Wed May 20 12:52:09 2020 +0200
1.3 @@ -7,7 +7,7 @@
1.4 (1) names of the problem-types and methods and their hierarchy
1.5 as subproblems.
1.6 names of problem-types are string lists (diss 5.3.), not shown
1.7 - here with exception of ["equation","univariate"] in order to
1.8 + here with exception of ["equation", "univariate"] in order to
1.9 indicate, that this particular problem needs refinement to a
1.10 more specific type of equation solvable by tan-square, etc.
1.11
1.12 @@ -19,7 +19,7 @@
1.13 introduce-a-new-variable
1.14 max-of-fun-on-interval max-of-fun-on-interval
1.15 derivative differentiate
1.16 - ["equation","univariate"] tan-square
1.17 + ["equation", "univariate"] tan-square
1.18
1.19 find-values find-values
1.20
1.21 @@ -32,11 +32,11 @@
1.22 {given = ["fixed_values (cs::bool list)"],
1.23 where_= ["foldl (op &) True (map is_equality cs)",
1.24 "foldl (op &) True (map (Not o ((op <=) #0) o Rhs) cs)"],
1.25 - find=["maximum m","values_for (ms::real list)"],
1.26 + find=["maximum m", "values_for (ms::real list)"],
1.27 with_=["Ex_frees ((foldl (op &) True (r#RS)) & \
1.28 \ (ALL m'. (subst (m,m') (foldl (op &) True (r#RS)) \
1.29 \ --> m' <= m)))"],
1.30 - relate=["max_relation r","additionalRels RS"]};
1.31 + relate=["max_relation r", "additionalRels RS"]};
1.32 (* ^^^ is exponenation *)
1.33
1.34 (* the functions Ex_frees, Rhs provide for the instantiation below *)
1.35 @@ -45,7 +45,7 @@
1.36 {given = ["fixed_values (R = #7)"],
1.37 where_= ["is_equality (R = #7)",
1.38 "Not (R <= #0)"],
1.39 - find =["maximum A","values_for [a,b]"],
1.40 + find =["maximum A", "values_for [a,b]"],
1.41 with_ =["EX A. A = a*b & (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2 \
1.42 \ (ALL A'. A' = a*b & (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2 \
1.43 \ --> A' <= A)))"],
1.44 @@ -57,7 +57,7 @@
1.45 {given = ["fixed_values (R = #7)"],
1.46 where_= ["is_equality (R = #7)",
1.47 "Not (R <= #0)"],
1.48 - find =["maximum A","values_for [A]"],
1.49 + find =["maximum A", "values_for [A]"],
1.50 with_ =["EX a b alpha. A = a*b & \
1.51 \ a = #2*R*sin alpha & b =#2*R*cos alpha &\
1.52 \ (ALL A'. A' = a*b & a = #2*R*sin alpha & b =#2*R*cos alpha \
1.53 @@ -70,7 +70,7 @@
1.54 (* make-fun *)
1.55 (* -------- *)
1.56 (* problem-type *)
1.57 -{given = ["equality (lhs = rhs)","bound_variable v","equalities es"],
1.58 +{given = ["equality (lhs = rhs)", "bound_variable v", "equalities es"],
1.59 where_= [],
1.60 find = ["function_term lhs_"],
1.61 with_ = [(*???*)],
1.62 @@ -78,7 +78,7 @@
1.63 (*the _ in lhs is used to transfer the lhs-identifier of equality*)
1.64
1.65 (* (1) instantiation for make-explicit-and-substitute *)
1.66 -{given = ["equality A = a * b","bound_variable a",
1.67 +{given = ["equality A = a * b", "bound_variable a",
1.68 "equalities [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"],
1.69 where_= [],
1.70 find = ["function_term A_"(*=(a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))*)],
1.71 @@ -86,7 +86,7 @@
1.72 relate= []};
1.73
1.74 (* (2) instantiation for introduce-a-new-variable *)
1.75 -{given = ["equality A = a * b","bound_variable alpha",
1.76 +{given = ["equality A = a * b", "bound_variable alpha",
1.77 "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
1.78 where_= [],
1.79 find = ["function_term A_"(*=(#2*R*sin alpha *#2*R*cos alpha)*)],
1.80 @@ -97,7 +97,7 @@
1.81 (* max-of-fun-on-interval *)
1.82 (* ---------------------- *)
1.83 (* problem-type *)
1.84 -{given = ["function_term t","bound_variable v",
1.85 +{given = ["function_term t", "bound_variable v",
1.86 "domain {x::real. lower_bound <= x & x <= upper_bound}"],
1.87 where_= [],
1.88 find = ["maximums ms"],
1.89 @@ -133,7 +133,7 @@
1.90 (* derivative *)
1.91 (* ---------- *)
1.92 (* problem-type *)
1.93 -{given = ["function_term t","bound_variable bdv"],
1.94 +{given = ["function_term t", "bound_variable bdv"],
1.95 where_= [],
1.96 find = ["derivative t'"],
1.97 with_ = ["t' is_derivative_of (%bdv. t)"],
1.98 @@ -141,11 +141,11 @@
1.99 (*the ' in t' is used to transfer the identifier from function_term*)
1.100
1.101
1.102 -(* ["equation","univariate"] *)
1.103 +(* ["equation", "univariate"] *)
1.104 (* ------------------------- *)
1.105 (* problem-type *)
1.106 {given = ["equality (lhs = rhs)",
1.107 - "bound_variable v","error_bound eps"],
1.108 + "bound_variable v", "error_bound eps"],
1.109 where_= [],
1.110 find = ["solutions S"],
1.111 with_ = ["ALL s. s : S --> || (%v. lhs) s - (%v. rhs) s || <= eps"],
1.112 @@ -155,7 +155,7 @@
1.113 (* find-values *)
1.114 (* ----------- *)
1.115 (* problem-type *)
1.116 -{given = ["max_relation r","additionalRels RS"],
1.117 +{given = ["max_relation r", "additionalRels RS"],
1.118 where_= [],
1.119 find = ["values_for VS"],
1.120 with_ = [(*???*)],
1.121 @@ -202,7 +202,7 @@
1.122
1.123
1.124 max-of-fun-on-interval + derivative ->
1.125 - #given.["equation","univariate"]
1.126 + #given.["equation", "univariate"]
1.127 ----------------------------------------------------------------
1.128 derivative.#find "derivative t'" -> "equality (lhs = rhs)"
1.129 (* t'= #0 *)
1.130 @@ -231,11 +231,11 @@
1.131 val pbltyp = {given=["fixed_values (cs::bool list)"],
1.132 where_=["foldl (op &) True (map is_equality cs)",
1.133 "foldl (op &) True (map (Not o ((op <=) #0) o Rhs) cs)"],
1.134 - find=["maximum m","values_for (ms::real list)"],
1.135 + find=["maximum m", "values_for (ms::real list)"],
1.136 with_=["Ex_frees ((foldl (op &) True (r#rs)) & \
1.137 \ (ALL m'. (subst (m,m') (foldl (op &) True (r#rs)) \
1.138 \ --> m' <= m)))"],
1.139 - relate=["max_relation r","additionalRels rs"]}:string ppc;
1.140 + relate=["max_relation r", "additionalRels rs"]}:string ppc;
1.141 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
1.142 "coil";
1.143 val org = ["fixed_values [R=(R::real)]",
1.144 @@ -250,7 +250,7 @@
1.145 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"];
1.146 val chkorg = map (the o (parse thy)) org;
1.147 val pbl = {given=["fixed_values [R=(R::real)]"],where_=[],
1.148 - find=["maximum A","values_for [a,b]"],
1.149 + find=["maximum A", "values_for [a,b]"],
1.150 with_=["EX alpha. A=#2*a*b - a^^^#2 & \
1.151 \ a=#2*R*sin alpha & b=#2*R*cos alpha & \
1.152 \ (ALL A'. A'=#2*a*b - a^^^#2 & a=#2*R*sin alpha & b=#2*R*cos alpha \
1.153 @@ -261,12 +261,12 @@
1.154 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
1.155
1.156 "met --- maximum_by_differentiation ---";
1.157 -val met = {given=["fixed_values (cs::bool list)","bound_variable v",
1.158 +val met = {given=["fixed_values (cs::bool list)", "bound_variable v",
1.159 "domain {x::real. lower_bound <= x & x <= upper_bound}",
1.160 "approximation apx"],
1.161 where_=[],
1.162 - find=["maximum m","values_for (ms::real list)",
1.163 - "function_term t","max_argument mx"],
1.164 + find=["maximum m", "values_for (ms::real list)",
1.165 + "function_term t", "max_argument mx"],
1.166 with_=["Ex_frees ((foldl (op &) True (rs::bool list)) & \
1.167 \ (ALL m'. (subst (m,m') (foldl (op &) True rs) \
1.168 \ --> m' <= m))) & \
1.169 @@ -281,13 +281,13 @@
1.170 (* subproblem [(hd #relate root, equality),
1.171 (bound_variable formalization, bound_variable),
1.172 (tl #relate root, equalities)] *)
1.173 -val pbltyp = {given=["equality e","bound_variable v", "equalities es"],
1.174 +val pbltyp = {given=["equality e", "bound_variable v", "equalities es"],
1.175 where_=[],
1.176 find=["function_term t"],with_=[(*???*)],
1.177 relate=[(*???*)]}: string ppc;
1.178 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
1.179 "coil";
1.180 -val pbl = {given=["equality (A=#2*a*b - a^^^#2)","bound_variable alpha",
1.181 +val pbl = {given=["equality (A=#2*a*b - a^^^#2)", "bound_variable alpha",
1.182 "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
1.183 where_=[],
1.184 find=["function_term t"],
1.185 @@ -295,13 +295,13 @@
1.186 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
1.187
1.188 "met --- make_explicit_and_substitute ---";
1.189 -val met = {given=["equality e","bound_variable v", "equalities es"],
1.190 +val met = {given=["equality e", "bound_variable v", "equalities es"],
1.191 where_=[],
1.192 find=["function_term t"],with_=[(*???*)],
1.193 relate=[(*???*)]}: string ppc;
1.194 val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met;
1.195 "met --- introduce_a_new_variable ---";
1.196 -val met = {given=["equality e","bound_variable v", "substitutions es"],
1.197 +val met = {given=["equality e", "bound_variable v", "substitutions es"],
1.198 where_=[],
1.199 find=["function_term t"],with_=[(*???*)],
1.200 relate=[(*???*)]}: string ppc;
1.201 @@ -309,7 +309,7 @@
1.202
1.203
1.204 "pbltyp --- max_of_fun_on_interval ---";
1.205 -val pbltyp = {given=["function_term t","bound_variable v",
1.206 +val pbltyp = {given=["function_term t", "bound_variable v",
1.207 "domain {x::real. lower_bound <= x & x <= upper_bound}"],
1.208 where_=[],
1.209 find=["maximums ms"],
1.210 @@ -320,7 +320,7 @@
1.211 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
1.212 "coil";
1.213 val pbl = {given=["function_term #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \
1.214 - \ (#2*R*sin alpha)^^^#2","bound_variable alpha",
1.215 + \ (#2*R*sin alpha)^^^#2", "bound_variable alpha",
1.216 "domain {x::real. #0 <= x & x <= pi}"],where_=[],
1.217 find=["maximums [#1234]"],with_=[],relate=[]}: string ppc;
1.218 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;