1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Fri Jun 17 12:15:09 2022 +0200
1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Sat Jun 18 12:34:29 2022 +0200
1.3 @@ -60,7 +60,7 @@
1.4 "maximum. + Figure",
1.5 (["[r = 7]", "[A, [u, v]]", "[A = 2 \<sqdot> u \<sqdot> v - u 2 , ( 2 u ) 2 + ( 2 v ) 2 = r 2 ]",
1.6 "{0 < .. < r}"]: TermC.as_string list,
1.7 - (*TODO: compare paper + test/../DiffApp: more than one list of Model_Def.form_model? *)
1.8 + (*TODO: compare paper + test/../Diff_App: more than one list of Model_Def.form_model? *)
1.9 ("Diff_App", ["univariate_calculus", "Optimisation"],
1.10 ["Optimisation", "by_univariate_calculus"]): References.T)): example) example_store
1.11 \<close> ML \<open>
2.1 --- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Fri Jun 17 12:15:09 2022 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,429 +0,0 @@
2.4 -(* use"test-coil-kernel.sml";
2.5 - W.N.22.11.99
2.6 -
2.7 -*)
2.8 -
2.9 -(* vvv--- geht nicht wegen fun-types
2.10 -parse thy "case maxmin of is_max => (m' <= m) | is_min => (m <= m')";
2.11 -parse thy "if maxmin = is_max then (m' <= m) else (m <= m')";
2.12 -parse thy "if a=b then a else b";
2.13 -parse thy "maxmin = is_max";
2.14 -parse thy "maxmin =!= is_max";
2.15 - ^^^--- geht nicht wegen fun-types *)
2.16 -
2.17 -"pbltyp --- maximum ---";
2.18 -val pbltyp = {given=["fixedValues (cs::bool list)"],
2.19 - where_=[(*"foldl (op &) True (map is_equality cs)",
2.20 - "foldl (op &) True (map (Not o ((op <=) #0) o Rhs) cs)"*)],
2.21 - find=["maximum m", "values_for (ms::real list)"],
2.22 - with_=[(*"Ex_frees ((foldl (op &) True (r#rs)) & \
2.23 - \ (ALL m'. (subst (m,m') (foldl (op &) True (r#rs)) \
2.24 - \ --> m' <= m)))"*)],
2.25 - relate=["max_relation r", "additionalRels rs"]}:string ppc;
2.26 -val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
2.27 -"coil";
2.28 -val org = ["fixedValues [R=(R::real)]",
2.29 - "boundVariable a", "boundVariable b", "boundVariable alpha",
2.30 - "domain {x::real. #0 <= x & x <= #2*R}",
2.31 - "domain {x::real. #0 <= x & x <= #2*R}",
2.32 - "domain {x::real. #0 <= x & x <= pi}",
2.33 - "errorBound (eps = #1//#1000)",
2.34 - "maximum A",
2.35 - (*"max_relation A=#2*a*b - a \<up> #2",*)
2.36 - "relations [A=#2*a*b - a \<up> #2, (a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2]",
2.37 - "relations [A=#2*a*b - a \<up> #2, (a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2]",
2.38 - "relations [A=#2*a*b - a \<up> #2, a=#2*R*sin alpha, b=#2*R*cos alpha]"];
2.39 -val chkorg = map (the o (parse thy)) org;
2.40 -val pbl = {given=["fixedValues [R=(R::real)]"],where_=[],
2.41 - find=["maximum A", "values_for [a,b]"],
2.42 - with_=[(* incompat.w. parse, ok with parseold: theory -> string -> cterm option
2.43 - "EX alpha. A=#2*a*b - a \<up> #2 & \
2.44 - \ a=#2*R*sin alpha & b=#2*R*cos alpha & \
2.45 - \ (ALL A'. A'=#2*a*b - a \<up> #2 & a=#2*R*sin alpha \
2.46 - \ & b=#2*R*cos alpha \
2.47 - \ --> A' <= A)"*)],
2.48 - relate=["relations [A=#2*a*b - a \<up> #2, a=#2*R*sin alpha, b=#2*R*cos alpha]"]
2.49 - }: string ppc;
2.50 -val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
2.51 -
2.52 -"met --- maximum_by_differentiation ---";
2.53 -val met = {given=["fixedValues (cs::bool list)", "boundVariable v",
2.54 - "domain {x::real. lower_bound <= x & x<=upper_bound}",
2.55 - "errorBound epsilon"],
2.56 - where_=[],
2.57 - find=["maximum m", "valuesFor (ms::bool list)",
2.58 - "function_term t", "max_argument mx"],
2.59 - with_=[(* incompat.w. parse, ok with parseold: theory -> string -> cterm option
2.60 - "Ex_frees ((foldl (op &) True (mr#ars)) & \
2.61 - \ (ALL m'. (subst (m,m') (foldl (op &) True (mr#ars))\
2.62 - \ --> m' <= m))) & \
2.63 - \m = (%v. t) mx & \
2.64 - \( ALL x. lower_bound <= x & x <= upper_bound \
2.65 - \ --> (%v. t) x <= m)"*)],
2.66 - relate=["max_relation mr",
2.67 - "additionalRels ars"]}: string ppc;
2.68 -val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) met;
2.69 -
2.70 -"data --- maximum_by_differentiation ---";
2.71 -val met = {given=["fixedValues [R=(R::real)]", "boundVariable alpha",
2.72 - "domain {x::real. #0 <= x & x <= pi//#2}",
2.73 - "errorBound (eps = #1//#1000)"],
2.74 - where_=[],
2.75 - find=["maximum A", "valuesFor [a=Undef]",
2.76 - "function_term t", "max_argument mx"],
2.77 - with_=[(* incompat.w. parse, ok with parseold: theory -> string -> cterm option
2.78 - "EX b alpha. A = #2*a*b - a \<up> #2 & \
2.79 - \ a = #2*R*sin alpha & \
2.80 - \ b = #2*R*cos alpha & \
2.81 - \ (ALL A'. A'= #2*a*b - a \<up> #2 & \
2.82 - \ a = #2*R*sin alpha & \
2.83 - \ b = #2*R*cos alpha --> A' <= A) & \
2.84 - \ A = (%alpha. t) mx & \
2.85 - \ (ALL x. #0 <= x & x <= pi --> \
2.86 - \ (%alpha. t) x <= A)"*)],
2.87 - relate=["max_relation mr",
2.88 - "additionalRels ars"]}: string ppc;
2.89 -val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) met;
2.90 -
2.91 -parseold: theory -> string -> cterm option;
2.92 -val (SOME ct) = parseold thy "EX b. (EX alpha. A = #2*a*b - a \<up> #2)";
2.93 -
2.94 -"pbltyp --- make_fun ---";
2.95 -(* subproblem [(hd #relate root, equality),
2.96 - (boundVariable formalization, boundVariable),
2.97 - (tl #relate root, equalities)] *)
2.98 -val pbltyp = {given=["equality e", "boundVariable v", "equalities es"],
2.99 - where_=[],
2.100 - find=["functionTerm t"],with_=[(*???*)],
2.101 - relate=[(*???*)]}: string ppc;
2.102 -val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
2.103 -"coil";
2.104 -val pbl = {given=["equality (A=#2*a*b - a \<up> #2)", "boundVariable alpha",
2.105 - "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
2.106 - where_=[],
2.107 - find=["functionTerm t"],
2.108 - with_=[],relate=[]}: string ppc;
2.109 -val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
2.110 -
2.111 -"met --- make_explicit_and_substitute ---";
2.112 -val met = {given=["equality e", "boundVariable v", "equalities es"],
2.113 - where_=[],
2.114 - find=["functionTerm t"],with_=[(*???*)],
2.115 - relate=[(*???*)]}: string ppc;
2.116 -val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met;
2.117 -"met --- introduce_a_new_variable ---";
2.118 -val met = {given=["equality e", "boundVariable v", "substitutions es"],
2.119 - where_=[],
2.120 - find=["functionTerm t"],with_=[(*???*)],
2.121 - relate=[(*???*)]}: string ppc;
2.122 -val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met;
2.123 -
2.124 -
2.125 -"pbltyp --- max_of_fun_on_interval ---";
2.126 -val pbltyp = {given=["functionTerm t", "boundVariable v",
2.127 - "domain {x::real. lower_bound <= x & x <= upper_bound}"],
2.128 - where_=[],
2.129 - find=["maximums ms"],
2.130 - with_=[(* incompat.w. parse, ok with parseold: theory -> string -> cterm option
2.131 - "ALL m. m : ms --> \
2.132 - \ (ALL x::real. lower_bound <= x & x <= upper_bound \
2.133 - \ --> (%v. t) x <= m)"*)],
2.134 - relate=[]}: string ppc;
2.135 -val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
2.136 -"coil";
2.137 -val pbl = {given=["functionTerm (f = #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \
2.138 - \ (#2*R*sin alpha) \<up> #2)", "boundVariable alpha",
2.139 - "domain {x::real. #0 <= x & x <= pi}"],where_=[],
2.140 - find=["maximums [#1234]"],with_=[],relate=[]}: string ppc;
2.141 -val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
2.142 -
2.143 -
2.144 -(* pbltyp --- max_of_fun --- *)
2.145 -(*
2.146 -{given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;
2.147 -val (SOME ct) = parse thy ;
2.148 -atomty (Thm.term_of ct);
2.149 -*)
2.150 -
2.151 -
2.152 -(* --- 14.1.00 ev. nicht ganz up to date bzg. oberem --- *)
2.153 -"p.114";
2.154 -val org = {given=["[u=(#12::real)]"],where_=[],
2.155 - find=["[a,(b::real)]"],with_=[],
2.156 - relate=["[is_max A=a*(b::real), #2*a+#2*b=(u::real)]"]}: string ppc;
2.157 -val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
2.158 -"p.116";
2.159 -val org = {given=["[c=#10, h=(#4::real)]"],where_=[],
2.160 - find=["[x,(y::real)]"],with_=[],
2.161 - relate=["[A=x*(y::real), c//h=x//(h-(y::real))]"]}: string ppc;
2.162 -val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
2.163 -"p.117";
2.164 -val org = {given=["[r=#5]"],where_=[],
2.165 - find=["[x,(y::real)]"],with_=[],
2.166 - relate=["[is_max #0=pi*x \<up> #2 + pi*x*(r::real)]"]}: string ppc;
2.167 -val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
2.168 -"#241";
2.169 -val org = {given=["[s=(#10::real)]"],where_=[],
2.170 - find=["[p::real]"],with_=[],
2.171 - relate=["[is_max p=n*m, s=n+(m::real)]"]}: string ppc;
2.172 -val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
2.173 -
2.174 -
2.175 -
2.176 -(* -------------- coil-kernel -------------- vor 19.1.00 *)
2.177 -(* --- subproblem: make-function-by-subst ~~~~~~~~~~~ *)
2.178 -(* --- subproblem: max-of-function *)
2.179 -(* --- subproblem: derivative *)
2.180 -(* --- subproblem: tan-quadrat-equation *)
2.181 -"-------------- coil-kernel --------------";
2.182 -val origin = ["A=#2*a*b - a \<up> #2",
2.183 - "a::real", "b::real", "{x. #0<x & x<R//#2}",
2.184 - "{(a//#2) \<up> #2 + (b//#2) \<up> #2 = (R//#2) \<up> #2}",
2.185 - "alpha::real", "{alpha::real. #0<alpha & alpha<pi//#2}",
2.186 - "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",
2.187 - "{R::real}"];
2.188 -(* --- for a isa-users-mail --- FIXME
2.189 -Goal "{x. x < a} = ?z";
2.190 -{x::'a. x < a} = ?z
2.191 -Goal "{x. x < #3} = {a}";
2.192 -{x::'a. x < (#3::'a)} = {a}
2.193 -Goal "{x. #3 < x} = ?z";
2.194 -Collect (op < (#3::'a)) = ?z
2.195 ----------------------------- *)
2.196 -
2.197 -val formals = map (the o (parse thy)) origin;
2.198 -
2.199 -val given = ["formula_for_max (lhs=rhs)", "boundVariable bdv",
2.200 - "interval {x. low < x & x < high}",
2.201 - "additional_conds ac", "constants cs"];
2.202 -val where_ = ["lhs is_atom", "bdv is_atom", "low is_atom", "high is_atom",
2.203 - "||| Vars equ ||| = ||| VarsSet ac ||| - ||| ac ||| + #1"];
2.204 -val find = ["f::real => real", "maxs::real set"];
2.205 -val with_ = [(* incompat.w. parse, ok with parseold: theory -> string -> cterm option
2.206 - "maxs = {m. low < m & m < high & \
2.207 - \ (m is_local_max_of (%bdv. f))}"*)];
2.208 -val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
2.209 -val givens = map (the o (parse thy)) given;
2.210 -
2.211 -"------- 1.1 -------";
2.212 -(* 5.3.00
2.213 -val formals = map (the o (parse thy)) ["A=#2*a*b - a \<up> #2",
2.214 - "a::real", "{x. #0<x & x<R//#2}",
2.215 - "{(a//#2) \<up> #2 + (b//#2) \<up> #2 = (R//#2) \<up> #2}",
2.216 - "{R::real}"];
2.217 -val tag__forms = chktyps thy (formals, givens);
2.218 -map ((atomty) o Thm.term_of) tag__forms;
2.219 -
2.220 -val formals = map (the o (parse thy)) ["A=#2*a*b - a \<up> #2",
2.221 - "alpha::real", "{alpha. #0<alpha & alpha<pi//#2}",
2.222 - "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",
2.223 - "{R::real}"];
2.224 -val tag__forms = chktyps thy (formals, givens);
2.225 -map ((atomty) o Thm.term_of) tag__forms;
2.226 -*)
2.227 -
2.228 -" --- subproblem: make-function-by-subst --- ";
2.229 -val origin = ["A=#2*a*b - a \<up> #2",
2.230 - "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",
2.231 - "{R::real}"];
2.232 -val formals = map (the o (parse thy)) origin;
2.233 -
2.234 -val given = ["equation (lhs=rhs)", "substitutions ss",
2.235 - "constants cs"];
2.236 -val where_ = [];
2.237 -val find = ["t::real"];
2.238 -val with_ = ["||| Vars t ||| = #1"];
2.239 -val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
2.240 -val givens = map (the o (parse thy)) given;
2.241 -(* 5.3.00
2.242 -val tag__forms = chktyps thy (formals, givens);
2.243 -map ((atomty) o Thm.term_of) tag__forms;
2.244 -*)
2.245 -" --- subproblem: max-of-function --- ";
2.246 -val origin = ["A = #2*(#2*R*(sin alpha))*(#2*R*(sin alpha)) - \
2.247 - \ (#2*R*(sin alpha)) \<up> #2",
2.248 - "{alpha. #0<alpha & alpha<pi//#2}",
2.249 - "{R::real}"];
2.250 -val formals = map (the o (parse thy)) origin;
2.251 -
2.252 -val given = ["equation (lhs=rhs)",
2.253 - "interval {x. low < x & x < high}",
2.254 - "constants cs"];
2.255 -val where_ = ["lhs is_atom", "low is_atom", "high is_atom"];
2.256 -val find = ["t::real"];
2.257 -val with_ = ["||| Vars t ||| = #1"];
2.258 -val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
2.259 -val givens = map (the o (parse thy)) given;
2.260 -(* 5.3.00
2.261 -val tag__forms = chktyps thy (formals, givens);
2.262 -map ((atomty) o Thm.term_of) tag__forms;
2.263 -*)
2.264 -" --- subproblem: derivative --- ";
2.265 -val origin = ["x \<up> #3-y \<up> #3+#-3*x+#12*y+#10", "x::real"];
2.266 -val formals = map (the o (parse thy)) origin;
2.267 -
2.268 -val given = ["functionTerm t",
2.269 - "boundVariable bdv"];
2.270 -val where_ = ["bdv is_atom"];
2.271 -val find = ["t'::real"];
2.272 -val with_ = ["t' is_derivative_of (%bdv. t)"];
2.273 -val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
2.274 -val givens = map (the o (parse thy)) given;
2.275 -(*
2.276 -val tag__forms = chktyps thy (formals, givens);
2.277 -map ((atomty) o Thm.term_of) tag__forms;
2.278 -*)
2.279 -" --- subproblem: tan-quadrat-equation --- ";
2.280 -val origin = ["#8*R \<up> #2*(cos alpha) \<up> #2 + #-8*R \<up> #2* \
2.281 - \ (cos alpha)*(sin alpha) + #8*R \<up> #2*(sin alpha) \<up> #2 = #0",
2.282 - "alpha::real", "#1//#1000"];
2.283 -val formals = map (the o (parse thy)) origin;
2.284 -
2.285 -val given = ["equation (a*(cos bdv) \<up> #2 + b*(cos bdv)*(sin bdv) + \
2.286 - \ c*(sin bdv) = #0)",
2.287 - "boundVariable bdv", "errorBound epsilon"];
2.288 -val where_ = ["bdv is_atom", "epsilon is_const_expr"];
2.289 -val find = ["L::real set"];
2.290 -val with_ = ["L = {x. || (%bdv. a*(cos bdv) \<up> #2 + b*(cos bdv)*(sin bdv) + \
2.291 - \ c*(sin bdv)) x || < epsilon}"];
2.292 -(* 5.3.00
2.293 -val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
2.294 -val givens = map (the o (parse thy)) given;
2.295 -val tag__forms = chktyps thy (formals, givens);
2.296 -map ((atomty) o Thm.term_of) tag__forms;
2.297 -*)
2.298 -(* use"test-coil-kernel.sml";
2.299 - *)
2.300 -
2.301 -
2.302 -" #################################################### ";
2.303 -" test specify ";
2.304 -" #################################################### ";
2.305 -
2.306 -
2.307 -val cts =
2.308 -["fixedValues [R=(R::real)]",
2.309 - "boundVariable a", "boundVariable b",
2.310 - "boundVariable alpha",
2.311 - "domain {x::real. #0 <= x & x <= #2*R}",
2.312 - "domain {x::real. #0 <= x & x <= #2*R}",
2.313 - "domain {x::real. #0 <= x & x <= pi//#2}",
2.314 - "errorBound (eps = #1//#1000)",
2.315 - "maximum A", "valuesFor [a=Undef]",
2.316 - (*"functionTerm t", "max_argument mx",
2.317 - "max_relation (A=#2*a*b - a \<up> #2)", *)
2.318 - "additionalRels [A=#2*a*b - a \<up> #2,(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2]",
2.319 - "additionalRels [A=#2*a*b - a \<up> #2,(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2]",
2.320 - "additionalRels [A=#2*a*b - a \<up> #2,a=#2*R*sin alpha, b=#2*R*cos alpha]"];
2.321 -val (dI',pI',mI')=
2.322 - ("DiffAppl",["Program", "maximum_of", "function"],MethodC.id_empty);
2.323 -val c = []:cid;
2.324 -
2.325 -(*
2.326 -val pbl = {given=["fixedValues [R=(R::real)]", "boundVariable alpha",
2.327 - "domain {x::real. #0 <= x & x <= pi//#2}",
2.328 - "errorBound (eps = #1//#1000)"],
2.329 - where_=[],
2.330 - find=["maximum A", "valuesFor [a=Undef]"(*,
2.331 - "functionTerm t", "max_argument mx"*)],
2.332 - with_=[],
2.333 - relate=["max_relation (A=#2*a*b - a \<up> #2)",
2.334 - "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2]",
2.335 - "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2]",
2.336 - "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
2.337 - }: string ppc;
2.338 -*)
2.339 -val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = Test_Code.CalcTreeTEST [(cts, (dI',pI',mI'))];
2.340 -
2.341 -val ct = "fixedValues [R=(R::real)]";
2.342 -(*l(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify(Add_Given ct) p c pt*)
2.343 -val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
2.344 -
2.345 -val ct = "boundVariable a";
2.346 -val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
2.347 -val ct = "boundVariable alpha";
2.348 -val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
2.349 -
2.350 -val ct = "domain {x::real. #0 <= x & x <= pi//#2}";
2.351 -val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
2.352 -
2.353 -val ct = "errorBound (eps = (#1::real) // #1000)";
2.354 -val ct = "maximum A";
2.355 -val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
2.356 -
2.357 -val ct = "valuesFor [a=Undef]";
2.358 -val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
2.359 -
2.360 -val ct = "max_relation ()";
2.361 -val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
2.362 -
2.363 -val ct = "relations [A=#2*a*b - a \<up> #2,(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2]";
2.364 -val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
2.365 -
2.366 -(* ... nxt = Specify_Domain ...
2.367 -val ct = "additionalRels [b=#2*R*cos alpha]";
2.368 -val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =
2.369 - specify(Add_Relation ct) p c pt;
2.370 -(*
2.371 -val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
2.372 -*)
2.373 -val ct = "additionalRels [a=#2*R*sin alpha]";
2.374 -val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =
2.375 - specify(Add_Relation ct) p c pt;
2.376 -(*
2.377 -val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
2.378 -*)
2.379 -*)
2.380 -(* --- tricky case (termlist interleaving variants):
2.381 -> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = Test_Code.CalcTreeTEST [(cts, (dI',pI',mI'))];
2.382 -
2.383 -> val ct = "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2, b=#2*R*cos alpha]";
2.384 -> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
2.385 -*)
2.386 -
2.387 -(* --- incomplete input ---
2.388 -> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = Test_Code.CalcTreeTEST [(cts, (dI',pI',mI'))];
2.389 -
2.390 -> val ct = "[R=(R::real)]";
2.391 -> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
2.392 -
2.393 -> val ct = "R=(R::real)";
2.394 -> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
2.395 -
2.396 -> val ct = "(R::real)";
2.397 -> specify nxt p c pt;
2.398 -*)
2.399 -
2.400 -
2.401 -" #################################################### ";
2.402 -" test do_ specify ";
2.403 -" #################################################### ";
2.404 -
2.405 -
2.406 -val cts = ["fixedValues [R=(R::real)]",
2.407 - "boundVariable a", "boundVariable b",
2.408 - "boundVariable alpha",
2.409 - "domain {x::real. #0 <= x & x <= #2*R}",
2.410 - "domain {x::real. #0 <= x & x <= #2*R}",
2.411 - "domain {x::real. #0 <= x & x <= pi//#2}",
2.412 - "errorBound (eps=#1//#1000)",
2.413 - "maximum A", "valuesFor [a=Undef]",
2.414 - (*"functionTerm t", "max_argument mx", *)
2.415 - "max_relation (A=#2*a*b - a \<up> #2)",
2.416 - "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2]",
2.417 - "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2]",
2.418 - "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"];
2.419 -val (dI',pI',mI')=
2.420 - ("DiffAppl",["DiffAppl", "test_maximum"],MethodC.id_empty);
2.421 -val p = e_pos'; val c = [];
2.422 -
2.423 -(*/------- Init_Proof replaced by Test_Code.CalcTreeTEST ------------------------------------\* )
2.424 -val (mI,m) = ("Init_Proof",Init_Proof (cts, (dI',pI',mI')));
2.425 -val (pst as (sc,pt,cl):pstate) = (Rule.Empty_Prog, e_ctree, []);
2.426 -val (p,_,f,nxt,_,(_,pt,_)) = do_ (mI,m) p c pst;
2.427 -(*val nxt = ("Add_Given",Add_Given "fixedValues [R = R]")*)
2.428 -
2.429 -val (p,_,Form' (PpcKF (_,_,ppc)),nxt,_,(_,pt,_)) =
2.430 - do_ nxt p c (Rule.Empty_Prog,pt,[]);
2.431 -(*val nxt = ("Add_Given",Add_Given "boundVariable a") *)
2.432 -( *\------- Init_Proof replaced by Test_Code.CalcTreeTEST ------------------------------------/*)
3.1 --- a/src/Tools/isac/Knowledge/DiffApp.sml Fri Jun 17 12:15:09 2022 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,104 +0,0 @@
3.4 -(* = DiffAppl.ML
3.5 - +++ outcommented tests
3.6 -*)
3.7 -
3.8 -
3.9 -
3.10 -(*
3.11 -> get_pbt ["DiffAppl", "maximum_of", "function"];
3.12 -> get_met ("Program", "max_on_interval_by_calculus");
3.13 -> !pbltypes;
3.14 - *)
3.15 -pbltypes:= overwritel (!pbltypes,
3.16 -[
3.17 - prep_pbt DiffAppl.thy
3.18 - (["DiffAppl", "maximum_of", "function"],
3.19 - [("#Given" ,"fixedValues f_ix"),
3.20 - ("#Find" ,"maximum m_"),
3.21 - ("#Find" ,"valuesFor v_s"),
3.22 - ("#Relate", "relations r_s") (*,
3.23 - ("#where" ,"foldl (op&) True (map (Not o ((op<=) #0) o Rhs) f_ix)"),
3.24 - ("#with" ,"Ex_frees ((foldl (op &) True r_s) & \
3.25 - \ (ALL m'. (subst (m_,m') (foldl (op &) True r_s) \
3.26 - \ --> m' <= m_)))") *)
3.27 - ]),
3.28 -
3.29 - prep_pbt DiffAppl.thy
3.30 - (["DiffAppl", "make", "function"],
3.31 - [("#Given" ,"functionOf f_f"),
3.32 - ("#Given" ,"boundVariable v_v"),
3.33 - ("#Given" ,"equalities eqs"),
3.34 - ("#Find" ,"functionTerm f_0_")
3.35 - ]),
3.36 -
3.37 - prep_pbt DiffAppl.thy
3.38 - (["DiffAppl", "on_interval", "maximum_of", "function"],
3.39 - [("#Given" ,"functionTerm t_"),
3.40 - ("#Given" ,"boundVariable v_v"),
3.41 - ("#Given" ,"interval itv_"),
3.42 - ("#Find" ,"maxArgument v_0")
3.43 - ]),
3.44 -
3.45 - prep_pbt DiffAppl.thy
3.46 - (["DiffAppl", "find_values", "tool"],
3.47 - [("#Given" ,"maxArgument ma_"),
3.48 - ("#Given" ,"functionTerm f_f"),
3.49 - ("#Given" ,"boundVariable v_v"),
3.50 - ("#Find" ,"valuesFor vls_"),
3.51 - ("#Relate", "additionalRels r_s")
3.52 - ])
3.53 -]);
3.54 -
3.55 -
3.56 -methods:= overwritel (!methods,
3.57 -[
3.58 - (("DiffAppl", "max_by_calculus"),
3.59 - {ppc = prep_met DiffAppl.thy
3.60 - [("#Given" ,"fixedValues f_ix"),
3.61 - ("#Given" ,"boundVariable v_v"),
3.62 - ("#Given" ,"interval itv_"),
3.63 - ("#Given" ,"errorBound err_"),
3.64 - ("#Find" ,"maximum m_"),
3.65 - ("#Find" ,"valuesFor v_s"),
3.66 - ("#Relate", "relations r_s")
3.67 - ],
3.68 - rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
3.69 - scr =Rule.Empty_Prog} : met),
3.70 -
3.71 - (("DiffAppl", "make_fun_by_new_variable"),
3.72 - {ppc = prep_met DiffAppl.thy
3.73 - [("#Given" ,"functionOf f_f"),
3.74 - ("#Given" ,"boundVariable v_v"),
3.75 - ("#Given" ,"equalities eqs"),
3.76 - ("#Find" ,"functionTerm f_0_")
3.77 - ],
3.78 - rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
3.79 - scr =Rule.Empty_Prog} : met),
3.80 -
3.81 - (("DiffAppl", "make_fun_by_explicit"),
3.82 - {ppc = prep_met DiffAppl.thy
3.83 - [("#Given" ,"functionOf f_f"),
3.84 - ("#Given" ,"boundVariable v_v"),
3.85 - ("#Given" ,"equalities eqs"),
3.86 - ("#Find" ,"functionTerm f_0_")
3.87 - ],
3.88 - rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
3.89 - scr =Rule.Empty_Prog} : met),
3.90 -
3.91 - (("DiffAppl", "max_on_interval_by_calculus"),
3.92 - {ppc = prep_met DiffAppl.thy
3.93 - [("#Given" ,"functionTerm t_"),
3.94 - ("#Given" ,"boundVariable v_v"),
3.95 - ("#Given" ,"interval itv_"),
3.96 - ("#Given" ,"errorBound err_"),
3.97 - ("#Find" ,"maxArgument v_0")
3.98 - ],
3.99 - rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
3.100 - scr =Rule.Empty_Prog} : met),
3.101 -
3.102 - (("DiffAppl", "find_values"),
3.103 - {ppc = prep_met DiffAppl.thy
3.104 - [],
3.105 - rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
3.106 - scr =Rule.Empty_Prog} : met)
3.107 -]);
4.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Fri Jun 17 12:15:09 2022 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,196 +0,0 @@
4.4 -(* application of differential calculus
4.5 - Walther Neuper 2002
4.6 - (c) due to copyright terms
4.7 -*)
4.8 -
4.9 -theory DiffApp imports Diff begin
4.10 -
4.11 -consts
4.12 -
4.13 - dummy :: real
4.14 -
4.15 -fun filterVar :: \<open>real \<Rightarrow> 'a list \<Rightarrow> 'a list\<close>
4.16 - where
4.17 - filterVar_Nil: \<open>filterVar v [] = []\<close>
4.18 - | filterVar_Const: \<open>filterVar v (x # xs) =
4.19 - (if v \<in> set (Vars x) then x # (filterVar v xs) else filterVar v xs)\<close>
4.20 -
4.21 -
4.22 -text \<open>WN.6.5.03: old decisions in this file partially are being changed
4.23 - in a quick-and-dirty way to make scripts run: Maximum_value,
4.24 - Make_fun_by_new_variable, Make_fun_by_explicit.
4.25 -found to be reconsidered:
4.26 -- descriptions (Input_Descript.thy)
4.27 -- penv: really need term list; or just rerun the whole example with num/var
4.28 -- mk_arg, arguments_from_model ... env in script different from penv ?
4.29 -- L = SubProblem eq ... show some vars on the worksheet ? (other means for
4.30 - referencing are labels (no on worksheet))
4.31 -
4.32 -WN.6.5.03 quick-and-dirty: mk_arg, arguments_from_model just make most convenient env
4.33 - from penv as is.
4.34 -\<close>
4.35 -
4.36 -ML \<open>
4.37 -val eval_rls = prep_rls' (
4.38 - Rule_Def.Repeat {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI),
4.39 - erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
4.40 - rules = [
4.41 - \<^rule_thm>\<open>refl\<close>,
4.42 - \<^rule_thm>\<open>order_refl\<close>,
4.43 - \<^rule_thm>\<open>radd_left_cancel_le\<close>,
4.44 - \<^rule_thm>\<open>not_true\<close>,
4.45 - \<^rule_thm>\<open>not_false\<close>,
4.46 - \<^rule_thm>\<open>and_true\<close>,
4.47 - \<^rule_thm>\<open>and_false\<close>,
4.48 - \<^rule_thm>\<open>or_true\<close>,
4.49 - \<^rule_thm>\<open>or_false\<close>,
4.50 - \<^rule_thm>\<open>and_commute\<close>,
4.51 - \<^rule_thm>\<open>or_commute\<close>,
4.52 -
4.53 - \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
4.54 - \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
4.55 -
4.56 - \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
4.57 - \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
4.58 - \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
4.59 - \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")],
4.60 - scr = Rule.Empty_Prog
4.61 - });
4.62 -\<close>
4.63 -rule_set_knowledge eval_rls = \<open>eval_rls\<close>
4.64 -
4.65 -(** problems **)
4.66 -
4.67 -problem pbl_fun_max : "maximum_of/function" =
4.68 - \<open>Rule_Set.empty\<close>
4.69 - Given: "fixedValues f_ix"
4.70 - Find: "maximum m_m" "valuesFor v_s"
4.71 - Relate: "relations r_s"
4.72 -
4.73 -problem pbl_fun_make : "make/function" =
4.74 - \<open>Rule_Set.empty\<close>
4.75 - Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
4.76 - Find: "functionEq f_1"
4.77 -
4.78 -problem pbl_fun_max_expl : "by_explicit/make/function" =
4.79 - \<open>Rule_Set.empty\<close>
4.80 - Method_Ref: "DiffApp/make_fun_by_explicit"
4.81 - Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
4.82 - Find: "functionEq f_1"
4.83 -
4.84 -problem pbl_fun_max_newvar : "by_new_variable/make/function" =
4.85 - \<open>Rule_Set.empty\<close>
4.86 - Method_Ref: "DiffApp/make_fun_by_new_variable"
4.87 - Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
4.88 - (*WN.12.5.03: precond for distinction still missing*)
4.89 - Find: "functionEq f_1"
4.90 -
4.91 -problem pbl_fun_max_interv : "on_interval/maximum_of/function" =
4.92 - \<open>Rule_Set.empty\<close>
4.93 - Given: "functionEq t_t" "boundVariable v_v" "interval i_tv"
4.94 - (*WN.12.5.03: precond for distinction still missing*)
4.95 - Find: "maxArgument v_0"
4.96 -
4.97 -problem pbl_tool : "tool" =
4.98 - \<open>Rule_Set.empty\<close>
4.99 -
4.100 -problem pbl_tool_findvals : "find_values/tool" =
4.101 - \<open>Rule_Set.empty\<close>
4.102 - Given: "maxArgument m_ax" "functionEq f_f" "boundVariable v_v"
4.103 - Find: "valuesFor v_ls"
4.104 - Relate: "additionalRels r_s"
4.105 -
4.106 -
4.107 -(** methods, scripts not yet implemented **)
4.108 -
4.109 -method met_diffapp : "DiffApp" =
4.110 - \<open>{rew_ord'="tless_true", rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
4.111 - crls = Atools_erls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}\<close>
4.112 -
4.113 -partial_function (tailrec) maximum_value ::
4.114 - "bool list \<Rightarrow> real \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> real set \<Rightarrow> bool \<Rightarrow> bool list"
4.115 - where
4.116 -"maximum_value f_ix m_m r_s v_v itv_v e_rr =
4.117 - (let e_e = (hd o (filterVar m_m)) r_s;
4.118 - t_t = if 1 < Length r_s
4.119 - then SubProblem (''DiffApp'', [''make'', ''function''],[''no_met''])
4.120 - [REAL m_m, REAL v_v, BOOL_LIST r_s]
4.121 - else (hd r_s);
4.122 - m_x = SubProblem (''DiffApp'', [''on_interval'', ''maximum_of'', ''function''],
4.123 - [''DiffApp'', ''max_on_interval_by_calculus''])
4.124 - [BOOL t_t, REAL v_v, REAL_SET itv_v]
4.125 - in SubProblem (''DiffApp'',[''find_values'', ''tool''], [''Isac_Knowledge'', ''find_values''])
4.126 - [REAL m_x, REAL (rhs t_t), REAL v_v, REAL m_m, BOOL_LIST (dropWhile (ident e_e) r_s)])"
4.127 -
4.128 -method met_diffapp_max : "DiffApp/max_by_calculus" =
4.129 - \<open>{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=prog_expr,prls=Rule_Set.empty, crls = eval_rls,
4.130 - errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}\<close>
4.131 - Program: maximum_value.simps
4.132 - Given: "fixedValues f_ix" "maximum m_m" "relations r_s" "boundVariable v_v"
4.133 - "interval i_tv" "errorBound e_rr"
4.134 - Find: "valuesFor v_s"
4.135 - Relate:
4.136 -
4.137 -partial_function (tailrec) make_fun_by_new_variable :: "real => real => bool list => bool"
4.138 - where
4.139 -"make_fun_by_new_variable f_f v_v eqs =
4.140 - (let h_h = (hd o (filterVar f_f)) eqs;
4.141 - e_s = dropWhile (ident h_h) eqs;
4.142 - v_s = dropWhile (ident f_f) (Vars h_h);
4.143 - v_1 = NTH 1 v_s;
4.144 - v_2 = NTH 2 v_s;
4.145 - e_1 = (hd o (filterVar v_1)) e_s;
4.146 - e_2 = (hd o (filterVar v_2)) e_s;
4.147 - s_1 = SubProblem (''DiffApp'', [''univariate'', ''equation''], [''no_met''])
4.148 - [BOOL e_1, REAL v_1];
4.149 - s_2 = SubProblem (''DiffApp'', [''univariate'', ''equation''], [''no_met''])
4.150 - [BOOL e_2, REAL v_2]
4.151 - in Substitute [(v_1 = (rhs o hd) s_1), (v_2 = (rhs o hd) s_2)] h_h)"
4.152 -
4.153 -method met_diffapp_funnew : "DiffApp/make_fun_by_new_variable" =
4.154 - \<open>{rew_ord'="tless_true",rls'=eval_rls,srls=prog_expr,prls=Rule_Set.empty, calc=[], crls = eval_rls,
4.155 - errpats = [], nrls = norm_Rational(*,asm_rls=[],asm_thm=[]*)}\<close>
4.156 - Program: make_fun_by_new_variable.simps
4.157 - Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
4.158 - Find: "functionEq f_1"
4.159 -
4.160 -partial_function (tailrec) make_fun_by_explicit :: "real => real => bool list => bool"
4.161 - where
4.162 -"make_fun_by_explicit f_f v_v eqs =
4.163 - (let h_h = (hd o (filterVar f_f)) eqs;
4.164 - e_1 = hd (dropWhile (ident h_h) eqs);
4.165 - v_s = dropWhile (ident f_f) (Vars h_h);
4.166 - v_1 = hd (dropWhile (ident v_v) v_s);
4.167 - s_1 = SubProblem(''DiffApp'', [''univariate'', ''equation''], [''no_met''])
4.168 - [BOOL e_1, REAL v_1]
4.169 - in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "
4.170 -
4.171 -method met_diffapp_funexp : "DiffApp/make_fun_by_explicit" =
4.172 - \<open>{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=prog_expr,prls=Rule_Set.empty, crls = eval_rls,
4.173 - errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}\<close>
4.174 - Program: make_fun_by_explicit.simps
4.175 - Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
4.176 - Find: "functionEq f_1"
4.177 -
4.178 -method met_diffapp_max_oninterval : "DiffApp/max_on_interval_by_calculus" =
4.179 - \<open>{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
4.180 - errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}\<close>
4.181 - Given: "functionEq t_t" "boundVariable v_v" "interval i_tv" (*"errorBound e_rr"*)
4.182 - Find: "maxArgument v_0"
4.183 -
4.184 -method met_diffapp_findvals : "DiffApp/find_values" =
4.185 - \<open>{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
4.186 - errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)}\<close>
4.187 -
4.188 -ML \<open>
4.189 -\<close> ML \<open>
4.190 -val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [
4.191 - \<^rule_thm>\<open>filterVar_Const\<close>,
4.192 - \<^rule_thm>\<open>filterVar_Nil\<close>];
4.193 -\<close>
4.194 -rule_set_knowledge prog_expr = \<open>prog_expr\<close>
4.195 -ML \<open>
4.196 -\<close> ML \<open>
4.197 -\<close> ML \<open>
4.198 -\<close>
4.199 -end
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/Tools/isac/Knowledge/Diff_App.thy Sat Jun 18 12:34:29 2022 +0200
5.3 @@ -0,0 +1,203 @@
5.4 +(* application of differential calculus
5.5 + Walther Neuper 2002
5.6 + (c) due to copyright terms
5.7 +*)
5.8 +
5.9 +theory Diff_App imports Diff begin
5.10 +
5.11 +consts
5.12 +
5.13 + dummy :: real
5.14 +
5.15 +fun filterVar :: \<open>real \<Rightarrow> 'a list \<Rightarrow> 'a list\<close>
5.16 + where
5.17 + filterVar_Nil: \<open>filterVar v [] = []\<close>
5.18 + | filterVar_Const: \<open>filterVar v (x # xs) =
5.19 + (if v \<in> set (Vars x) then x # (filterVar v xs) else filterVar v xs)\<close>
5.20 +
5.21 +
5.22 +text \<open>WN.6.5.03: old decisions in this file partially are being changed
5.23 + in a quick-and-dirty way to make scripts run: Maximum_value,
5.24 + Make_fun_by_new_variable, Make_fun_by_explicit.
5.25 +found to be reconsidered:
5.26 +- descriptions (Input_Descript.thy)
5.27 +- penv: really need term list; or just rerun the whole example with num/var
5.28 +- mk_arg, arguments_from_model ... env in script different from penv ?
5.29 +- L = SubProblem eq ... show some vars on the worksheet ? (other means for
5.30 + referencing are labels (no on worksheet))
5.31 +
5.32 +WN.6.5.03 quick-and-dirty: mk_arg, arguments_from_model just make most convenient env
5.33 + from penv as is.
5.34 +\<close>
5.35 +
5.36 +ML \<open>
5.37 +val eval_rls = prep_rls' (
5.38 + Rule_Def.Repeat {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI),
5.39 + erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
5.40 + rules = [
5.41 + \<^rule_thm>\<open>refl\<close>,
5.42 + \<^rule_thm>\<open>order_refl\<close>,
5.43 + \<^rule_thm>\<open>radd_left_cancel_le\<close>,
5.44 + \<^rule_thm>\<open>not_true\<close>,
5.45 + \<^rule_thm>\<open>not_false\<close>,
5.46 + \<^rule_thm>\<open>and_true\<close>,
5.47 + \<^rule_thm>\<open>and_false\<close>,
5.48 + \<^rule_thm>\<open>or_true\<close>,
5.49 + \<^rule_thm>\<open>or_false\<close>,
5.50 + \<^rule_thm>\<open>and_commute\<close>,
5.51 + \<^rule_thm>\<open>or_commute\<close>,
5.52 +
5.53 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
5.54 + \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
5.55 +
5.56 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
5.57 + \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
5.58 + \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
5.59 + \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")],
5.60 + scr = Rule.Empty_Prog
5.61 + });
5.62 +\<close>
5.63 +rule_set_knowledge eval_rls = \<open>eval_rls\<close>
5.64 +
5.65 +(** problems **)
5.66 +
5.67 +problem pbl_fun_max : "maximum_of/function" =
5.68 + \<open>Rule_Set.empty\<close>
5.69 + Given: "fixedValues f_ix"
5.70 + Find: "maximum m_m" "valuesFor v_s"
5.71 + Relate: "relations r_s"
5.72 +
5.73 +problem pbl_fun_make : "make/function" =
5.74 + \<open>Rule_Set.empty\<close>
5.75 + Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
5.76 + Find: "functionEq f_1"
5.77 +
5.78 +problem pbl_fun_max_expl : "by_explicit/make/function" =
5.79 + \<open>Rule_Set.empty\<close>
5.80 + Method_Ref: "Diff_App/make_fun_by_explicit"
5.81 + Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
5.82 + Find: "functionEq f_1"
5.83 +
5.84 +problem pbl_fun_max_newvar : "by_new_variable/make/function" =
5.85 + \<open>Rule_Set.empty\<close>
5.86 + Method_Ref: "Diff_App/make_fun_by_new_variable"
5.87 + Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
5.88 + (*WN.12.5.03: precond for distinction still missing*)
5.89 + Find: "functionEq f_1"
5.90 +
5.91 +problem pbl_fun_max_interv : "on_interval/maximum_of/function" =
5.92 + \<open>Rule_Set.empty\<close>
5.93 + Given: "functionEq t_t" "boundVariable v_v" "interval i_tv"
5.94 + (*WN.12.5.03: precond for distinction still missing*)
5.95 + Find: "maxArgument v_0"
5.96 +
5.97 +problem pbl_tool : "tool" =
5.98 + \<open>Rule_Set.empty\<close>
5.99 +
5.100 +problem pbl_tool_findvals : "find_values/tool" =
5.101 + \<open>Rule_Set.empty\<close>
5.102 + Given: "maxArgument m_ax" "functionEq f_f" "boundVariable v_v"
5.103 + Find: "valuesFor v_ls"
5.104 + Relate: "additionalRels r_s"
5.105 +
5.106 +ML \<open>
5.107 +\<close> text \<open>
5.108 +Problem.from_store ["univariate_calculus", "Optimisation"]
5.109 +\<close> ML \<open>
5.110 +\<close>
5.111 +
5.112 +(** methods, scripts not yet implemented **)
5.113 +
5.114 +method met_diffapp : "Diff_App" =
5.115 + \<open>{rew_ord'="tless_true", rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
5.116 + crls = Atools_erls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}\<close>
5.117 +
5.118 +partial_function (tailrec) maximum_value ::
5.119 + "bool list \<Rightarrow> real \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> real set \<Rightarrow> bool \<Rightarrow> bool list"
5.120 + where
5.121 +"maximum_value f_ix m_m r_s v_v itv_v e_rr =
5.122 + (let e_e = (hd o (filterVar m_m)) r_s;
5.123 + t_t = if 1 < Length r_s
5.124 + then SubProblem (''Diff_App'', [''make'', ''function''],[''no_met''])
5.125 + [REAL m_m, REAL v_v, BOOL_LIST r_s]
5.126 + else (hd r_s);
5.127 + m_x = SubProblem (''Diff_App'', [''on_interval'', ''maximum_of'', ''function''],
5.128 + [''Diff_App'', ''max_on_interval_by_calculus''])
5.129 + [BOOL t_t, REAL v_v, REAL_SET itv_v]
5.130 + in SubProblem (''Diff_App'',[''find_values'', ''tool''], [''Isac_Knowledge'', ''find_values''])
5.131 + [REAL m_x, REAL (rhs t_t), REAL v_v, REAL m_m, BOOL_LIST (dropWhile (ident e_e) r_s)])"
5.132 +
5.133 +method met_diffapp_max : "Diff_App/max_by_calculus" =
5.134 + \<open>{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=prog_expr,prls=Rule_Set.empty, crls = eval_rls,
5.135 + errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}\<close>
5.136 + Program: maximum_value.simps
5.137 + Given: "fixedValues f_ix" "maximum m_m" "relations r_s" "boundVariable v_v"
5.138 + "interval i_tv" "errorBound e_rr"
5.139 + Find: "valuesFor v_s"
5.140 + Relate:
5.141 +
5.142 +partial_function (tailrec) make_fun_by_new_variable :: "real => real => bool list => bool"
5.143 + where
5.144 +"make_fun_by_new_variable f_f v_v eqs =
5.145 + (let h_h = (hd o (filterVar f_f)) eqs;
5.146 + e_s = dropWhile (ident h_h) eqs;
5.147 + v_s = dropWhile (ident f_f) (Vars h_h);
5.148 + v_1 = NTH 1 v_s;
5.149 + v_2 = NTH 2 v_s;
5.150 + e_1 = (hd o (filterVar v_1)) e_s;
5.151 + e_2 = (hd o (filterVar v_2)) e_s;
5.152 + s_1 = SubProblem (''Diff_App'', [''univariate'', ''equation''], [''no_met''])
5.153 + [BOOL e_1, REAL v_1];
5.154 + s_2 = SubProblem (''Diff_App'', [''univariate'', ''equation''], [''no_met''])
5.155 + [BOOL e_2, REAL v_2]
5.156 + in Substitute [(v_1 = (rhs o hd) s_1), (v_2 = (rhs o hd) s_2)] h_h)"
5.157 +
5.158 +method met_diffapp_funnew : "Diff_App/make_fun_by_new_variable" =
5.159 + \<open>{rew_ord'="tless_true",rls'=eval_rls,srls=prog_expr,prls=Rule_Set.empty, calc=[], crls = eval_rls,
5.160 + errpats = [], nrls = norm_Rational(*,asm_rls=[],asm_thm=[]*)}\<close>
5.161 + Program: make_fun_by_new_variable.simps
5.162 + Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
5.163 + Find: "functionEq f_1"
5.164 +
5.165 +partial_function (tailrec) make_fun_by_explicit :: "real => real => bool list => bool"
5.166 + where
5.167 +"make_fun_by_explicit f_f v_v eqs =
5.168 + (let h_h = (hd o (filterVar f_f)) eqs;
5.169 + e_1 = hd (dropWhile (ident h_h) eqs);
5.170 + v_s = dropWhile (ident f_f) (Vars h_h);
5.171 + v_1 = hd (dropWhile (ident v_v) v_s);
5.172 + s_1 = SubProblem(''Diff_App'', [''univariate'', ''equation''], [''no_met''])
5.173 + [BOOL e_1, REAL v_1]
5.174 + in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "
5.175 +
5.176 +method met_diffapp_funexp : "Diff_App/make_fun_by_explicit" =
5.177 + \<open>{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=prog_expr,prls=Rule_Set.empty, crls = eval_rls,
5.178 + errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}\<close>
5.179 + Program: make_fun_by_explicit.simps
5.180 + Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
5.181 + Find: "functionEq f_1"
5.182 +
5.183 +method met_diffapp_max_oninterval : "Diff_App/max_on_interval_by_calculus" =
5.184 + \<open>{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
5.185 + errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}\<close>
5.186 + Given: "functionEq t_t" "boundVariable v_v" "interval i_tv" (*"errorBound e_rr"*)
5.187 + Find: "maxArgument v_0"
5.188 +
5.189 +method met_diffapp_findvals : "Diff_App/find_values" =
5.190 + \<open>{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
5.191 + errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)}\<close>
5.192 +
5.193 +ML \<open>
5.194 +\<close> text \<open>
5.195 +MethodC.from_store ["Optimisation", "by_univariate_calculus"]
5.196 +\<close> ML \<open>
5.197 +val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [
5.198 + \<^rule_thm>\<open>filterVar_Const\<close>,
5.199 + \<^rule_thm>\<open>filterVar_Nil\<close>];
5.200 +\<close>
5.201 +rule_set_knowledge prog_expr = \<open>prog_expr\<close>
5.202 +ML \<open>
5.203 +\<close> ML \<open>
5.204 +\<close> ML \<open>
5.205 +\<close>
5.206 +end
6.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Fri Jun 17 12:15:09 2022 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sat Jun 18 12:34:29 2022 +0200
6.3 @@ -3,7 +3,7 @@
6.4 (c) copyright due to lincense terms.
6.5 *)
6.6
6.7 -theory Inverse_Z_Transform imports PolyEq DiffApp Partial_Fractions begin
6.8 +theory Inverse_Z_Transform imports PolyEq Diff_App Partial_Fractions begin
6.9
6.10 axiomatization where \<comment> \<open>TODO: new variables on the rhs enforce replacement by substitution\<close>
6.11 rule1: "1 = \<delta>[n]" and
7.1 --- a/src/Tools/isac/Knowledge/Isac_Knowledge.thy Fri Jun 17 12:15:09 2022 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Isac_Knowledge.thy Sat Jun 18 12:34:29 2022 +0200
7.3 @@ -6,7 +6,7 @@
7.4 imports
7.5 (**) "$ISABELLE_ISAC/BridgeLibisabelle/BridgeLibisabelle" (*remove after devel.of BridgeJEdit*)
7.6 (** )"$ISABELLE_ISAC/BridgeJEdit/BridgeJEdit" ( *activate after devel.of BridgeJEdit*)
7.7 - PolyMinus PolyEq Vect DiffApp Biegelinie AlgEin InsSort
7.8 + PolyMinus PolyEq Vect Diff_App Biegelinie AlgEin InsSort
7.9 DiophantEq Inverse_Z_Transform Test
7.10 begin
7.11
8.1 --- a/src/Tools/isac/ProgLang/Program.thy Fri Jun 17 12:15:09 2022 +0200
8.2 +++ b/src/Tools/isac/ProgLang/Program.thy Sat Jun 18 12:34:29 2022 +0200
8.3 @@ -15,7 +15,7 @@
8.4 subsection \<open>General constants: TODO shift to appropriate files\<close>
8.5 consts
8.6 Arbfix :: "real"
8.7 - Undef :: "real" (* WN190823 probably an outdated design for DiffApp *)
8.8 + Undef :: "real" (* WN190823 probably an outdated design for Diff_App *)
8.9 bool_undef :: "bool"
8.10
8.11 subsection \<open>Theorems specific for evaluation of assumptions of theorems/rules\<close>
9.1 --- a/src/Tools/isac/TODO.thy Fri Jun 17 12:15:09 2022 +0200
9.2 +++ b/src/Tools/isac/TODO.thy Sat Jun 18 12:34:29 2022 +0200
9.3 @@ -395,7 +395,7 @@
9.4 \item xxx
9.5 \item this has been written in one go:
9.6 \begin{itemize}
9.7 - \item reconsidering I_Model.max_vt, use problem with meth ["DiffApp", "max_by_calculus"]
9.8 + \item reconsidering I_Model.max_vt, use problem with meth ["Diff_App", "max_by_calculus"]
9.9 \item reconsider add_field': where is it used for what? Shift into mk_oris
9.10 \item reconsider match_itms_oris: where is it used for what? max_vt ONLY???
9.11 \item in Specify_Method search root-oris for items (e.g. "errorBound"), #1# in survey
10.1 --- a/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Fri Jun 17 12:15:09 2022 +0200
10.2 +++ b/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Sat Jun 18 12:34:29 2022 +0200
10.3 @@ -26,5 +26,5 @@
10.4 "----------- fun met_hierarchy2file ------------------------------------------------------------";
10.5 if Pbl_Met_Hierarchy.met_hierarchy2file "dummy/path/" =
10.6 ("dummy/path/met_hierarchy.xml",
10.7 - "<NODE>\n <ID> method hierarchy </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_ROOT </CONTENTREF>\n <NODE>\n <ID> empty_meth_id </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_empty </CONTENTREF>\n </NODE>\n <NODE>\n <ID> simplification </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_tsimp </CONTENTREF>\n <NODE>\n <ID> for_polynomials </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_simp_poly </CONTENTREF>\n <NODE>\n <ID> with_minus </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_simp_poly_minus </CONTENTREF>\n </NODE>\n <NODE>\n <ID> with_parentheses </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_simp_poly_parenth </CONTENTREF>\n </NODE>\n <NODE>\n <ID> with_parentheses_mult </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_simp_poly_parenth_mult </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> of_rationals </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_simp_rat </CONTENTREF>\n <NODE>\n <ID> to_partial_fraction </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_partial_fraction </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> probe </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_probe </CONTENTREF>\n <NODE>\n <ID> fuer_polynom </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_probe_poly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> fuer_bruch </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_probe_bruch </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Equation </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_equ </CONTENTREF>\n <NODE>\n <ID> solve_log </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_equ_log </CONTENTREF>\n </NODE>\n <NODE>\n <ID> fromFunction </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_equ_fromfun </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> RootEq </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_rooteq </CONTENTREF>\n <NODE>\n <ID> norm_sq_root_equation </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_rooteq_norm </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_sq_root_equation </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_rooteq_sq </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_right_sq_root_equation </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_rooteq_sq_right </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_left_sq_root_equation </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_rooteq_sq_left </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> LinEq </ID>\n <NO> 6 </NO>\n <CONTENTREF> met_eqlin </CONTENTREF>\n <NODE>\n <ID> solve_lineq_equation </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_eq_lin </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> RatEq </ID>\n <NO> 7 </NO>\n <CONTENTREF> met_rateq </CONTENTREF>\n <NODE>\n <ID> solve_rat_equation </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_rat_eq </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> RootRatEq </ID>\n <NO> 8 </NO>\n <CONTENTREF> met_rootrateq </CONTENTREF>\n <NODE>\n <ID> elim_rootrat_equation </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_rootrateq_elim </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> PolyEq </ID>\n <NO> 9 </NO>\n <CONTENTREF> met_polyeq </CONTENTREF>\n <NODE>\n <ID> normalise_poly </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_polyeq_norm </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d0_polyeq_equation </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_polyeq_d0 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d1_polyeq_equation </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_polyeq_d1 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_equation </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_polyeq_d22 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_bdvonly_equation </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_polyeq_d2_bdvonly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_sqonly_equation </ID>\n <NO> 6 </NO>\n <CONTENTREF> met_polyeq_d2_sqonly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_pq_equation </ID>\n <NO> 7 </NO>\n <CONTENTREF> met_polyeq_d2_pq </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_abc_equation </ID>\n <NO> 8 </NO>\n <CONTENTREF> met_polyeq_d2_abc </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d3_polyeq_equation </ID>\n <NO> 9 </NO>\n <CONTENTREF> met_polyeq_d3 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> complete_square </ID>\n <NO> 10 </NO>\n <CONTENTREF> met_polyeq_complsq </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> diff </ID>\n <NO> 10 </NO>\n <CONTENTREF> met_diff </CONTENTREF>\n <NODE>\n <ID> differentiate_on_R </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_diff_onR </CONTENTREF>\n </NODE>\n <NODE>\n <ID> diff_simpl </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_diff_simpl </CONTENTREF>\n </NODE>\n <NODE>\n <ID> differentiate_equality </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_diff_equ </CONTENTREF>\n </NODE>\n <NODE>\n <ID> after_simplification </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_diff_after_simp </CONTENTREF>\n </NODE>\n <NODE>\n <ID> integration </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_diffint </CONTENTREF>\n <NODE>\n <ID> named </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_diffint_named </CONTENTREF>\n </NODE>\n <NODE>\n <ID> test </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_testint </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> EqSystem </ID>\n <NO> 11 </NO>\n <CONTENTREF> met_eqsys </CONTENTREF>\n <NODE>\n <ID> top_down_substitution </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_eqsys_topdown </CONTENTREF>\n <NODE>\n <ID> 2x2 </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_eqsys_topdown_2x2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> 4x4 </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_eqsys_topdown_4x4 </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> normalise </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_eqsys_norm </CONTENTREF>\n <NODE>\n <ID> 2x2 </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_eqsys_norm_2x2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> 4x4 </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_eqsys_norm_4x4 </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> IntegrierenUndKonstanteBestimmen </ID>\n <NO> 12 </NO>\n <CONTENTREF> met_biege </CONTENTREF>\n <NODE>\n <ID> 2xIntegrieren </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_biege_intconst_2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> 4x4System </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_biege_intconst_4 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> 1xIntegrieren </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_biege_intconst_1 </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> IntegrierenUndKonstanteBestimmen2 </ID>\n <NO> 13 </NO>\n <CONTENTREF> met_biege_2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> Biegelinien </ID>\n <NO> 14 </NO>\n <CONTENTREF> met_biege2 </CONTENTREF>\n <NODE>\n <ID> ausBelastung </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_biege_ausbelast </CONTENTREF>\n </NODE>\n <NODE>\n <ID> setzeRandbedingungenEin </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_biege_setzrand </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Berechnung </ID>\n <NO> 15 </NO>\n <CONTENTREF> met_algein </CONTENTREF>\n <NODE>\n <ID> erstNumerisch </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_algein_numsym_1num </CONTENTREF>\n </NODE>\n <NODE>\n <ID> erstSymbolisch </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_algein_symnum </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Programming </ID>\n <NO> 16 </NO>\n <CONTENTREF> met_Programming </CONTENTREF>\n <NODE>\n <ID> SORT </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_Prog_sort </CONTENTREF>\n <NODE>\n <ID> insertion </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_Prog_sort_ins </CONTENTREF>\n </NODE>\n <NODE>\n <ID> insertion_steps </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_Prog_sort_ins_steps </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> Test </ID>\n <NO> 17 </NO>\n <CONTENTREF> met_test </CONTENTREF>\n <NODE>\n <ID> solve_linear </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_test_solvelin </CONTENTREF>\n </NODE>\n <NODE>\n <ID> sqrt-equ-test </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_test_sqrt </CONTENTREF>\n </NODE>\n <NODE>\n <ID> squ-equ-test-subpbl1 </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_test_squ_sub </CONTENTREF>\n </NODE>\n <NODE>\n <ID> square_equation1 </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_test_eq1 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> square_equation2 </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_test_squ2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> square_equation </ID>\n <NO> 6 </NO>\n <CONTENTREF> met_test_squeq </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_plain_square </ID>\n <NO> 7 </NO>\n <CONTENTREF> met_test_eq_plain </CONTENTREF>\n </NODE>\n <NODE>\n <ID> norm_univar_equation </ID>\n <NO> 8 </NO>\n <CONTENTREF> met_test_norm_univ </CONTENTREF>\n </NODE>\n <NODE>\n <ID> intsimp </ID>\n <NO> 9 </NO>\n <CONTENTREF> met_test_intsimp </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_diophant </ID>\n <NO> 10 </NO>\n <CONTENTREF> met_test_diophant </CONTENTREF>\n </NODE>\n <NODE>\n <ID> test_calculate </ID>\n <NO> 11 </NO>\n <CONTENTREF> met_testcal </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> DiffApp </ID>\n <NO> 18 </NO>\n <CONTENTREF> met_diffapp </CONTENTREF>\n <NODE>\n <ID> max_by_calculus </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_diffapp_max </CONTENTREF>\n </NODE>\n <NODE>\n <ID> make_fun_by_new_variable </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_diffapp_funnew </CONTENTREF>\n </NODE>\n <NODE>\n <ID> make_fun_by_explicit </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_diffapp_funexp </CONTENTREF>\n </NODE>\n <NODE>\n <ID> max_on_interval_by_calculus </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_diffapp_max_oninterval </CONTENTREF>\n </NODE>\n <NODE>\n <ID> find_values </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_diffapp_findvals </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> SignalProcessing </ID>\n <NO> 19 </NO>\n <CONTENTREF> met_SP </CONTENTREF>\n <NODE>\n <ID> Z_Transform </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_SP_Ztrans </CONTENTREF>\n <NODE>\n <ID> Inverse </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_SP_Ztrans_inv </CONTENTREF>\n </NODE>\n <NODE>\n <ID> Inverse_sub </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_SP_Ztrans_inv_sub </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n</NODE>")
10.8 + "<NODE>\n <ID> method hierarchy </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_ROOT </CONTENTREF>\n <NODE>\n <ID> empty_meth_id </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_empty </CONTENTREF>\n </NODE>\n <NODE>\n <ID> simplification </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_tsimp </CONTENTREF>\n <NODE>\n <ID> for_polynomials </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_simp_poly </CONTENTREF>\n <NODE>\n <ID> with_minus </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_simp_poly_minus </CONTENTREF>\n </NODE>\n <NODE>\n <ID> with_parentheses </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_simp_poly_parenth </CONTENTREF>\n </NODE>\n <NODE>\n <ID> with_parentheses_mult </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_simp_poly_parenth_mult </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> of_rationals </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_simp_rat </CONTENTREF>\n <NODE>\n <ID> to_partial_fraction </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_partial_fraction </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> probe </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_probe </CONTENTREF>\n <NODE>\n <ID> fuer_polynom </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_probe_poly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> fuer_bruch </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_probe_bruch </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Equation </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_equ </CONTENTREF>\n <NODE>\n <ID> solve_log </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_equ_log </CONTENTREF>\n </NODE>\n <NODE>\n <ID> fromFunction </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_equ_fromfun </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> RootEq </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_rooteq </CONTENTREF>\n <NODE>\n <ID> norm_sq_root_equation </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_rooteq_norm </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_sq_root_equation </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_rooteq_sq </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_right_sq_root_equation </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_rooteq_sq_right </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_left_sq_root_equation </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_rooteq_sq_left </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> LinEq </ID>\n <NO> 6 </NO>\n <CONTENTREF> met_eqlin </CONTENTREF>\n <NODE>\n <ID> solve_lineq_equation </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_eq_lin </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> RatEq </ID>\n <NO> 7 </NO>\n <CONTENTREF> met_rateq </CONTENTREF>\n <NODE>\n <ID> solve_rat_equation </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_rat_eq </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> RootRatEq </ID>\n <NO> 8 </NO>\n <CONTENTREF> met_rootrateq </CONTENTREF>\n <NODE>\n <ID> elim_rootrat_equation </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_rootrateq_elim </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> PolyEq </ID>\n <NO> 9 </NO>\n <CONTENTREF> met_polyeq </CONTENTREF>\n <NODE>\n <ID> normalise_poly </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_polyeq_norm </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d0_polyeq_equation </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_polyeq_d0 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d1_polyeq_equation </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_polyeq_d1 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_equation </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_polyeq_d22 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_bdvonly_equation </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_polyeq_d2_bdvonly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_sqonly_equation </ID>\n <NO> 6 </NO>\n <CONTENTREF> met_polyeq_d2_sqonly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_pq_equation </ID>\n <NO> 7 </NO>\n <CONTENTREF> met_polyeq_d2_pq </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_abc_equation </ID>\n <NO> 8 </NO>\n <CONTENTREF> met_polyeq_d2_abc </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d3_polyeq_equation </ID>\n <NO> 9 </NO>\n <CONTENTREF> met_polyeq_d3 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> complete_square </ID>\n <NO> 10 </NO>\n <CONTENTREF> met_polyeq_complsq </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> diff </ID>\n <NO> 10 </NO>\n <CONTENTREF> met_diff </CONTENTREF>\n <NODE>\n <ID> differentiate_on_R </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_diff_onR </CONTENTREF>\n </NODE>\n <NODE>\n <ID> diff_simpl </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_diff_simpl </CONTENTREF>\n </NODE>\n <NODE>\n <ID> differentiate_equality </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_diff_equ </CONTENTREF>\n </NODE>\n <NODE>\n <ID> after_simplification </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_diff_after_simp </CONTENTREF>\n </NODE>\n <NODE>\n <ID> integration </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_diffint </CONTENTREF>\n <NODE>\n <ID> named </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_diffint_named </CONTENTREF>\n </NODE>\n <NODE>\n <ID> test </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_testint </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> EqSystem </ID>\n <NO> 11 </NO>\n <CONTENTREF> met_eqsys </CONTENTREF>\n <NODE>\n <ID> top_down_substitution </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_eqsys_topdown </CONTENTREF>\n <NODE>\n <ID> 2x2 </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_eqsys_topdown_2x2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> 4x4 </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_eqsys_topdown_4x4 </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> normalise </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_eqsys_norm </CONTENTREF>\n <NODE>\n <ID> 2x2 </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_eqsys_norm_2x2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> 4x4 </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_eqsys_norm_4x4 </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> IntegrierenUndKonstanteBestimmen </ID>\n <NO> 12 </NO>\n <CONTENTREF> met_biege </CONTENTREF>\n <NODE>\n <ID> 2xIntegrieren </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_biege_intconst_2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> 4x4System </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_biege_intconst_4 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> 1xIntegrieren </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_biege_intconst_1 </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> IntegrierenUndKonstanteBestimmen2 </ID>\n <NO> 13 </NO>\n <CONTENTREF> met_biege_2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> Biegelinien </ID>\n <NO> 14 </NO>\n <CONTENTREF> met_biege2 </CONTENTREF>\n <NODE>\n <ID> ausBelastung </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_biege_ausbelast </CONTENTREF>\n </NODE>\n <NODE>\n <ID> setzeRandbedingungenEin </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_biege_setzrand </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Berechnung </ID>\n <NO> 15 </NO>\n <CONTENTREF> met_algein </CONTENTREF>\n <NODE>\n <ID> erstNumerisch </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_algein_numsym_1num </CONTENTREF>\n </NODE>\n <NODE>\n <ID> erstSymbolisch </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_algein_symnum </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Programming </ID>\n <NO> 16 </NO>\n <CONTENTREF> met_Programming </CONTENTREF>\n <NODE>\n <ID> SORT </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_Prog_sort </CONTENTREF>\n <NODE>\n <ID> insertion </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_Prog_sort_ins </CONTENTREF>\n </NODE>\n <NODE>\n <ID> insertion_steps </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_Prog_sort_ins_steps </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> Test </ID>\n <NO> 17 </NO>\n <CONTENTREF> met_test </CONTENTREF>\n <NODE>\n <ID> solve_linear </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_test_solvelin </CONTENTREF>\n </NODE>\n <NODE>\n <ID> sqrt-equ-test </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_test_sqrt </CONTENTREF>\n </NODE>\n <NODE>\n <ID> squ-equ-test-subpbl1 </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_test_squ_sub </CONTENTREF>\n </NODE>\n <NODE>\n <ID> square_equation1 </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_test_eq1 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> square_equation2 </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_test_squ2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> square_equation </ID>\n <NO> 6 </NO>\n <CONTENTREF> met_test_squeq </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_plain_square </ID>\n <NO> 7 </NO>\n <CONTENTREF> met_test_eq_plain </CONTENTREF>\n </NODE>\n <NODE>\n <ID> norm_univar_equation </ID>\n <NO> 8 </NO>\n <CONTENTREF> met_test_norm_univ </CONTENTREF>\n </NODE>\n <NODE>\n <ID> intsimp </ID>\n <NO> 9 </NO>\n <CONTENTREF> met_test_intsimp </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_diophant </ID>\n <NO> 10 </NO>\n <CONTENTREF> met_test_diophant </CONTENTREF>\n </NODE>\n <NODE>\n <ID> test_calculate </ID>\n <NO> 11 </NO>\n <CONTENTREF> met_testcal </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Diff_App </ID>\n <NO> 18 </NO>\n <CONTENTREF> met_diffapp </CONTENTREF>\n <NODE>\n <ID> max_by_calculus </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_diffapp_max </CONTENTREF>\n </NODE>\n <NODE>\n <ID> make_fun_by_new_variable </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_diffapp_funnew </CONTENTREF>\n </NODE>\n <NODE>\n <ID> make_fun_by_explicit </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_diffapp_funexp </CONTENTREF>\n </NODE>\n <NODE>\n <ID> max_on_interval_by_calculus </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_diffapp_max_oninterval </CONTENTREF>\n </NODE>\n <NODE>\n <ID> find_values </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_diffapp_findvals </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> SignalProcessing </ID>\n <NO> 19 </NO>\n <CONTENTREF> met_SP </CONTENTREF>\n <NODE>\n <ID> Z_Transform </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_SP_Ztrans </CONTENTREF>\n <NODE>\n <ID> Inverse </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_SP_Ztrans_inv </CONTENTREF>\n </NODE>\n <NODE>\n <ID> Inverse_sub </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_SP_Ztrans_inv_sub </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n</NODE>")
10.9 then () else error "met_hierarchy2file CHANGED: has a Method been updated?"
11.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Fri Jun 17 12:15:09 2022 +0200
11.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sat Jun 18 12:34:29 2022 +0200
11.3 @@ -952,8 +952,8 @@
11.4 "interval {x::real. 0 <= x & x <= pi}",
11.5 "errorBound (eps=(0::real))"]
11.6 (*specifying is not interesting for this example*)
11.7 - val spec = ("DiffApp", ["maximum_of", "function"],
11.8 - ["DiffApp", "max_by_calculus"]);
11.9 + val spec = ("Diff_App", ["maximum_of", "function"],
11.10 + ["Diff_App", "max_by_calculus"]);
11.11 (*the empty model with descriptions for user-guidance by Model_Problem*)
11.12 val empty_model = [P_Spec.Given ["fixedValues []"],
11.13 P_Spec.Find ["maximum", "valuesFor"],
11.14 @@ -977,7 +977,7 @@
11.15 !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
11.16 (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)
11.17 modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),
11.18 - "Problem (DiffApp.thy, [maximum_of, function])",
11.19 + "Problem (Diff_App.thy, [maximum_of, function])",
11.20 (*the head-form \<up> is not used for input here*)
11.21 [P_Spec.Given ["fixedValues [r=Arbfix]"(*new input*)],
11.22 P_Spec.Find ["maximum b"(*new input*), "valuesFor"],
11.23 @@ -1007,21 +1007,21 @@
11.24 P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
11.25 P_Spec.Relate ["relations [A=a*b, \
11.26 \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
11.27 - ("DiffApp", Problem.id_empty, MethodC.id_empty));
11.28 + ("Diff_App", Problem.id_empty, MethodC.id_empty));
11.29 modifyCalcHead 1 (([],Pbl), "not used here",
11.30 [P_Spec.Given ["fixedValues [r=Arbfix]"],
11.31 P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
11.32 P_Spec.Relate ["relations [A=a*b, \
11.33 \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
11.34 - ("DiffApp", ["maximum_of", "function"],
11.35 + ("Diff_App", ["maximum_of", "function"],
11.36 MethodC.id_empty));
11.37 modifyCalcHead 1 (([],Pbl), "not used here",
11.38 [P_Spec.Given ["fixedValues [r=Arbfix]"],
11.39 P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
11.40 P_Spec.Relate ["relations [A=a*b, \
11.41 \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
11.42 - ("DiffApp", ["maximum_of", "function"],
11.43 - ["DiffApp", "max_by_calculus"]));
11.44 + ("Diff_App", ["maximum_of", "function"],
11.45 + ["Diff_App", "max_by_calculus"]));
11.46 (*this final calcHead now has STATUS 'complete' !*)
11.47 DEconstrCalcTree 1;
11.48
12.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Fri Jun 17 12:15:09 2022 +0200
12.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Sat Jun 18 12:34:29 2022 +0200
12.3 @@ -388,8 +388,8 @@
12.4 "interval {x::real. 0 <= x & x <= pi}",
12.5 "errorBound (eps=(0::real))"]
12.6 (*specifying is not interesting for this example*)
12.7 - val spec = ("DiffApp", ["maximum_of", "function"],
12.8 - ["DiffApp", "max_by_calculus"]);
12.9 + val spec = ("Diff_App", ["maximum_of", "function"],
12.10 + ["Diff_App", "max_by_calculus"]);
12.11 (*the empty model with descriptions for user-guidance by Model_Problem*)
12.12 val empty_model = [Given ["fixedValues []"],
12.13 Find ["maximum", "valuesFor"],
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/test/Tools/isac/Knowledge/diff-app.sml Sat Jun 18 12:34:29 2022 +0200
13.3 @@ -0,0 +1,794 @@
13.4 +(* tests for IsacKnowledge/Diff_App
13.5 + author Walther Neuper 000301
13.6 + (c) due to copyright terms
13.7 +
13.8 + use"../smltest/IsacKnowledge/diffapp.sml";
13.9 + use"diffapp.sml";
13.10 +*)
13.11 +
13.12 +Rewrite.trace_on := false; (*true false*)
13.13 +"Contents----------------------------------------------";
13.14 +" Specify_Problem (match_itms_oris) ";
13.15 +" test specify, fmz <> [] ";
13.16 +" test specify, fmz = [] ";
13.17 +" problemtypes + formalizations ";
13.18 +"-------------------- ctree of {(a,b). is-max ... ----------------";
13.19 +"--------- me .. scripts for maximum-example ---------------------";
13.20 +"--------- autoCalc .. scripts for maximum-example ---------------";
13.21 +
13.22 +"--------------------- 30.4.03: maximum .. rewrite_set_ prog_expr ---------";
13.23 +"---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
13.24 +"---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
13.25 +
13.26 +
13.27 +
13.28 +
13.29 +
13.30 +" #################################################### ";
13.31 +" problemtypes + formalizations ";
13.32 +" #################################################### ";
13.33 +" -------------- [maximum_of,function] --------------- ";
13.34 +val pbt =
13.35 + ["fixedValues f_ix", "maximum m_m", "valuesFor v_s", "relations r_s"];
13.36 +(*=== inhibit exn 110722=============================================================
13.37 +map (the o (parseold thy)) pbt;
13.38 +=== inhibit exn 110722=============================================================*)
13.39 +val fmz =
13.40 + ["fixedValues [r=Arbfix]", "maximum A",
13.41 + "valuesFor [a,b]",
13.42 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
13.43 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
13.44 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
13.45 +
13.46 + "boundVariable a", "boundVariable b", "boundVariable alpha",
13.47 + "interval {x::real. 0 <= x & x <= 2*r}",
13.48 + "interval {x::real. 0 <= x & x <= 2*r}",
13.49 + "interval {x::real. 0 <= x & x <= pi}",
13.50 + "errorBound (eps=(0::real))"];
13.51 +(*=== inhibit exn 110722=============================================================
13.52 +map (the o (parseold thy)) fmz;
13.53 +" -------------- [make,function] -------------- ";
13.54 +=== inhibit exn 110722=============================================================*)
13.55 +val pbt =
13.56 + ["functionOf f_f", "boundVariable v_v", "equalities eqs",
13.57 + "functionTerm f_0_0"];
13.58 +(*=== inhibit exn 110722=============================================================
13.59 +map (the o (parseold thy)) pbt;
13.60 +val fmz12 =
13.61 + ["functionOf A", "boundVariable a", "boundVariable b",
13.62 + "equalities [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
13.63 + (*28.11.00: "functionTerm (A_0=Undef)"*)"functionTerm (Undef)"];
13.64 +map (the o (parseold thy)) fmz12;
13.65 +val fmz3 =
13.66 + ["functionOf A", "boundVariable a", "boundVariable b",
13.67 + "equalities [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
13.68 + (*28.11.00: "functionTerm (A_0=Undef)"*)"functionTerm (Undef)"];
13.69 +map (the o (parseold thy)) fmz3;
13.70 +" --------- [univar,equation] --------- ";
13.71 +val pbt =
13.72 + ["equality e_e", "solveFor v_v", "solutions v_i_i"];
13.73 +map (the o (parseold thy)) pbt;
13.74 +val fmz =
13.75 + ["equality ((a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2)",
13.76 + "solveFor b", "solutions b_i"];
13.77 +map (the o (parseold thy)) fmz;
13.78 +" ---- [on_interval,maximum_of,function] ---- ";
13.79 +val pbt =
13.80 + ["functionTerm t_t", "boundVariable v_v", "interval itv_v",
13.81 + "errorBound err_r", "maxArgument v_0"];
13.82 +map (the o (parseold thy)) pbt;
13.83 +val fmz12 =
13.84 + [(*28.11.00: "functionTerm (A_0 = a*sqrt(#4*r \<up> #2 - a \<up> #2))",*)
13.85 + "functionTerm (a*sqrt(4*r \<up> 2 - a \<up> 2))",
13.86 + (*28.11.00: "functionTerm (A_0 = b*sqrt(#4*r \<up> #2 - b \<up> #2))",*)
13.87 + "functionTerm (b*sqrt(4*r \<up> 2 - b \<up> 2))",
13.88 + "boundVariable a", "boundVariable b",
13.89 + "interval {x::real. 0 <= x & x <= 2*r}",
13.90 + "errorBound (eps=0)", "maxArgument (a_0=Undef)"];
13.91 +map (the o (parseold thy)) fmz12;
13.92 +val fmz3 =
13.93 + [(*28.11.00: "functionTerm (A_0 = (#2*r*sin alpha)*(#2*r*cos alpha))",*)
13.94 + "functionTerm ((2*r*sin alpha)*(2*r*cos alpha))",
13.95 + "boundVariable alpha",
13.96 + "interval {x::real. 0 <= x & x <= pi}",
13.97 + "errorBound (eps=0)", "maxArgument (a_0=Undef)"];
13.98 +map (the o (parseold thy)) fmz3;
13.99 +" --------- [derivative_of,function] --------- ";
13.100 +val pbt =
13.101 + ["functionTerm f_f", "boundVariable v_v", "derivative f_f'"];
13.102 +map (the o (parseold thy)) pbt;
13.103 +val fmz =
13.104 + [(*28.11.00: "functionTerm (A_0=a*#2*sqrt r \<up> #2 - (a//#2) \<up> #2)",*)
13.105 + "functionTerm (a*2*sqrt r \<up> 2 - (a/2) \<up> 2)",
13.106 + "boundVariable a",
13.107 + (*28.11.00: "derivative (A_0'=Undef)"*)"derivative (Undef)"];
13.108 +map (the o (parseold thy)) fmz;
13.109 +" --------- [find_values,tool] --------- ";
13.110 +val pbt =
13.111 + ["maxArgument ma_a", "functionTerm f_f", "boundVariable v_v",
13.112 + "valuesFor vls_s", "additionalRels r_s"];
13.113 +map (the o (parseold thy)) pbt;
13.114 +val fmz1 =
13.115 + ["maxArgument (a_0=(srqt 2)*r)",
13.116 + (*28.11.00: "functionTerm (A_0=a*#2*sqrt r \<up> #2 - (a//#2) \<up> #2)",*)
13.117 + "functionTerm (a*2*sqrt r \<up> 2 - (a/2) \<up> 2)",
13.118 + "boundVariable a",
13.119 + "valuesFor [a,b]", "maximum A",
13.120 + "additionalRels [(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"];
13.121 +map (the o (parseold thy)) fmz1;
13.122 +
13.123 +=== inhibit exn 110722=============================================================*)
13.124 +
13.125 +
13.126 +"-------------------- ctree of {(a,b). is-max ... --------------------------";
13.127 +"-------------------- ctree of {(a,b). is-max ... --------------------------";
13.128 +"-------------------- ctree of {(a,b). is-max ... --------------------------";
13.129 +
13.130 +(* --vvv-- ausgeliehen von test-root-equ/sml *)
13.131 +val loc = Istate.empty;
13.132 +val (dI',pI',mI') =
13.133 + ("Program",["sqroot-test", "univariate", "equation"],
13.134 + ["Program", "squ-equ-test2"]);
13.135 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
13.136 + "solveFor x", "errorBound (eps=0)",
13.137 + "solutions L"];
13.138 +(*
13.139 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
13.140 +val ((p,p_),_,_,_,_,(_,pt,_)) = CalcTreeTEST [fmz, (dI',pI',mI')))];
13.141 + -- \<up> -- ausgeliehen von test-root-equ/sml *)
13.142 +(*-------------- 9.6.03 --- cappend_ ... term -------irreparabler test
13.143 +val (pt,_) =
13.144 + cappend_problem EmptyPtree [] loc ([],(dI',pI',mI'), .....);
13.145 +val pos = (lev_on o lev_dn) [];
13.146 +(* val pos = ([1]) *)
13.147 +val (pt,_) = cappend_parent pt pos loc "{(a,b). is-max ..."
13.148 + Empty_Tac TransitiveB;
13.149 +val pos = (lev_on o lev_dn) pos;
13.150 +(*val pos = ([1,1])*)
13.151 +val (pt,_) = cappend_atomic pt pos loc "{(a,b). is-max ..."
13.152 + Empty_Tac ("[1,1]:{(a,b). is-extremum ...",[]) Complete;
13.153 +val pos = lev_on pos;
13.154 +(*val pos = ([1,2])*)
13.155 +val (pt,_) = cappend_atomic pt pos loc "{(a,b). is-extremum ..."
13.156 + Empty_Tac ("[1,2]:{(a,b). f_x(a,b) ...",[]) Complete;
13.157 +val pos = lev_up pos;
13.158 +(*val pos = ([1])*)
13.159 +val (pt,_) = append_result pt pos Istate.empty ("[1#]:{(a,b). f_x(a,b) ...",[])
13.160 + Complete;
13.161 +
13.162 +val pos = lev_on pos;
13.163 +(*val pos = ([2]) *)
13.164 +val (pt,_) = cappend_atomic pt pos loc "{(a,b). f_x(a,b) ..."
13.165 + Empty_Tac ("[2]:{(a,b). f_x & f_xx &...",[]) Complete;
13.166 +val pos = lev_on pos;
13.167 +(*al pos = [3] : pos*)
13.168 +val (pt,_) = cappend_parent pt pos loc "{(a,b). f_x & f_xx &..."
13.169 + Empty_Tac TransitiveB;
13.170 +val pos = (lev_on o lev_dn) pos;
13.171 +(*pos = ([3,1]) *)
13.172 +val (pt,_) = cappend_atomic pt pos loc "{(a,b). f_x & f_xx & ..."
13.173 + Empty_Tac ("[3,1]:{(a,b). f_x & f_xx } cup ...",[]) Complete;
13.174 +val pos = lev_on pos;
13.175 +(*pos = ([3,2]) *)
13.176 +val (pt,_) = cappend_atomic pt pos loc "{(a,b). f_x & f_xx } cup.."
13.177 + Empty_Tac ("[3,2]:{(a,b). f_x ..} cup ...",[]) Complete;
13.178 +
13.179 +val pos = lev_up pos;
13.180 +(*pos = ([3]) *)
13.181 +val (pt,_) = append_result pt pos Istate.empty ("[3#]:{(a,b). f_x ..} cup..",[])
13.182 + Complete;
13.183 +val pos = lev_on pos;
13.184 +(*val pos = [4] : pos *)
13.185 +val (pt,_) = cappend_parent pt pos loc "{(a,b). f_x ..} cup ..."
13.186 + Empty_Tac IntersectB;
13.187 +val pos = (lev_on o lev_dn) pos;
13.188 +(*val pos = ([4,1]) *)
13.189 +val (pt,_) = cappend_parent pt pos loc "set_1 = ..."
13.190 + Empty_Tac SequenceB;
13.191 +
13.192 +
13.193 +val pos = (lev_on o lev_dn) pos;
13.194 +(*val pos = ([4,1,1]) *)
13.195 +val (pt,_) = cappend_parent(*pbl*) pt pos loc"f_x = d/dx x \<up> 3 ..."
13.196 + Empty_Tac TransitiveB;
13.197 +val pos = (lev_on o lev_dn) pos;
13.198 +(*val pos = ([4,1,1,1]) *)
13.199 +val (pt,_) = cappend_parent pt pos loc "d/dx x \<up> 3 ..."
13.200 + Empty_Tac TransitiveB;
13.201 +val pos = (lev_on o lev_dn) pos;
13.202 +(*val pos = ([4,1,1,1,1]) *)
13.203 +val (pt,_) = cappend_atomic pt pos loc "d/dx x \<up> 3 ..."
13.204 + Empty_Tac ("[4,1,1,1,1]:3x \<up> 2 + d/dx ...",[]) Complete;
13.205 +val pos = lev_on pos;
13.206 +(*val pos = ([4,1,1,1,2]) *)
13.207 +val (pt,_) = cappend_atomic pt pos loc "3x \<up> 2 + d/dx ..."
13.208 + Empty_Tac ("[4,1,1,1,2]:3x \<up> 2 + 0 + d/dx ...",[]) Complete;
13.209 +val pos = lev_on pos;
13.210 +(*pos = ([4,1,1,1,3]) *)
13.211 +val (pt,_) = cappend_atomic pt pos loc "3x \<up> 2 + 0 + d/dx ..."
13.212 + Empty_Tac ("[4,1,1,1,3]:3x \<up> 2 + 0 -3 ...",[]) Complete;
13.213 +"--- 1 ---";
13.214 +val pos = lev_up pos;
13.215 +(*pos = ([4,1,1,1]) *)
13.216 +val (pt,_) = append_result pt pos Istate.empty ("[4,1,1,1#]:3x \<up> 2 -3.",[])Complete;
13.217 +"--- 2 ---";
13.218 +val pos = lev_up pos;
13.219 +(*val pos = ([4,1,1]) *)
13.220 +val (pt,_) = append_result pt pos Istate.empty ("[4,1,1#]:found 3x \<up> 2 -3 ...",[])
13.221 + Complete;
13.222 +"--- 3 ---";
13.223 +val pos = lev_on pos;
13.224 +(*val pos = ([4,1,2]+) *)
13.225 +val (pt,_) = cappend_parent(*pbl*) pt pos loc "f_y = d/dy x \<up> 3 ..."
13.226 + Empty_Tac TransitiveB;
13.227 +"--- 4 ---";
13.228 +writeln (pr_ctree pr_short pt);
13.229 +
13.230 +(*
13.231 +. ----- pblobj -----
13.232 +1. {(a,b). is-max ...
13.233 +1.1. {(a,b). is-max ...
13.234 +1.2. {(a,b). is-extremum ...
13.235 +2. {(a,b). f_x(a,b) ...
13.236 +3. {(a,b). f_x & f_xx &...
13.237 +3.1. {(a,b). f_x & f_xx & ...
13.238 +3.2. {(a,b). f_x & f_xx } cup..
13.239 +4. {(a,b). f_x ..} cup ...
13.240 +4.1. set_1 = ...
13.241 +4.1.1. f_x = d/dx x \<up> 3 ...
13.242 +4.1.1.1. d/dx x \<up> 3 ...
13.243 +4.1.1.1.1. d/dx x \<up> 3 ...
13.244 +4.1.1.1.2. 3x \<up> 2 + d/dx ...
13.245 +4.1.1.1.3. 3x \<up> 2 + 0 + d/dx ...
13.246 +4.1.2. f_y = d/dy x \<up> 3 ...
13.247 +
13.248 + use"test-max-surf1.sml";
13.249 + *)
13.250 +-------------- 9.6.03 --- cappend_ ... term -------irreparabler test---*)
13.251 +
13.252 +
13.253 +"--------- me .. scripts for maximum-example ---------------------";
13.254 +"--------- me .. scripts for maximum-example ---------------------";
13.255 +"--------- me .. scripts for maximum-example ---------------------";
13.256 +
13.257 +val fmz =
13.258 + ["fixedValues [r=Arbfix]", "maximum A",
13.259 + "valuesFor [a,b]",
13.260 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
13.261 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
13.262 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
13.263 +
13.264 + "boundVariable a", "boundVariable b", "boundVariable alpha",
13.265 + "interval {x::real. 0 <= x & x <= 2*r}",
13.266 + "interval {x::real. 0 <= x & x <= 2*r}",
13.267 + "interval {x::real. 0 <= x & x <= pi}",
13.268 + "errorBound (eps=(0::real))"];
13.269 +val (dI',pI',mI') =
13.270 + ("Diff_App",["maximum_of", "function"],
13.271 + ["Diff_App", "max_by_calculus"]);
13.272 +
13.273 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
13.274 +(*=== inhibit exn 110722=============================================================
13.275 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.276 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.277 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.278 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.279 +val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
13.280 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.281 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.282 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.283 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.284 +case nxt of (_, Specify_Method ["Diff_App", "max_by_calculus"]) => ()
13.285 + | _ => error "diffapp.sml: max-exp me, nxt = Specify_Method";
13.286 +
13.287 +val oris = fst3 (get_obj g_origin pt (fst p)); writeln(O_Model.to_string oris);
13.288 +val pits = get_obj g_pbl pt (fst p); writeln(I_Model.to_string ctxt pits);
13.289 +
13.290 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.291 +val mits = get_obj g_met pt (fst p); writeln(I_Model.to_string ctxt mits);
13.292 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.293 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.294 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.295 +case nxt of (_,Apply_Method ["Diff_App", "max_by_calculus"] ) => ()
13.296 + | _ => error "diffapp.sml: max-exp me, nxt = Apply_Method";
13.297 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.298 +=== inhibit exn 110722=============================================================*)
13.299 +
13.300 +(*since 0508 Apply_Method does the 1st step, if NONE implicit_take -------------
13.301 +(*val nxt = ("Subproblem",Subproblem ("Diff_App",["make", "function"]))*)
13.302 +val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn_G e;
13.303 +(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["make", "function"])*)
13.304 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.305 +(*val nxt = ("Model_Problem",Model_Problem ["by_explicit", "make", "function"])*)
13.306 +----------------------------------------------------------------------------*)
13.307 +case nxt of (Model_Problem(*["by_explicit", "make", "function"]*)) => ()
13.308 + | _ => error "diffapp.sml: max-exp me, nxt = Model_Problem";
13.309 +
13.310 +(*=== inhibit exn 110722=============================================================
13.311 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.312 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.313 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.314 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.315 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.316 +=== inhibit exn 110722=============================================================*)
13.317 +
13.318 +val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string oris);
13.319 +val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt pits);
13.320 +
13.321 +(*=== inhibit exn 110722=============================================================
13.322 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.323 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.324 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.325 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.326 +case nxt of (_, Apply_Method ["Diff_App", "make_fun_by_explicit"]) => ()
13.327 + | _ => error "diffapp.sml: max-exp Apply_Method ([1], Met) ";
13.328 +=== inhibit exn 110722=============================================================*)
13.329 +
13.330 +(*----since WN050901 (ie. corr. mathengine#nxt_specify_ ..Specify.find_next_step' Pbl->p_
13.331 +we get at ...
13.332 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.333 +...
13.334 +### associate: Not_Associated m= Subproblem' ,
13.335 + stac= Substitute
13.336 + [(b, (rhs o hd)
13.337 + (Subproblem (thy, [normalise, polynomial, univariate, equation])))]
13.338 + (hd (filterVar A [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]))
13.339 +*** tac_from_prog TODO: no match for Substitute
13.340 +*** [(b, (rhs o hd)
13.341 +*** (Subproblem (thy, [normalise, polynomial, univariate, equation])))]
13.342 +*** (hd (filterVar A [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]))
13.343 +Exception- ERROR raised
13.344 +
13.345 +############################################################################
13.346 +# presumerably didnt work before either, but not detected due to Emtpy_Tac #
13.347 +############################################################################
13.348 +
13.349 +(*val nxt = Subproblem ("Diff_App",["univariate", "equation"])) *)
13.350 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.351 +(*val nxt = Refine_Tacitly ["univariate", "equation"])*)
13.352 +
13.353 +val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string oris);
13.354 +val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt pits);
13.355 +
13.356 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.357 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.358 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.359 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.360 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.361 +(*val nxt = ("Apply_Method",Apply_Method ["PolyEq", "normalise_poly"])*)
13.362 +
13.363 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.364 +(*val f = Form' (Test_Out.FormKF (~1,EdUndef,3,Nundef,"A = a * b"))*)
13.365 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.366 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.367 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.368 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.369 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.370 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.371 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.372 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.373 +(*val f = Form' (Test_Out.FormKF (~1,EdUndef,4,Nundef,"[b = A / a]"))*)
13.374 +
13.375 +------------------------------------------------------------------------*)
13.376 +
13.377 +(*val f =
13.378 +Error' (Error_ "Refine_Tacitly [\"univariate\",\"equation\"] not applicable")*)
13.379 +
13.380 +
13.381 +(*----postponed.15.5.03 run scripts for maximum-example: univariate equation*)
13.382 +(*=== inhibit exn 110722=============================================================
13.383 +
13.384 +val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
13.385 +=== inhibit exn 110722=============================================================*)
13.386 +
13.387 +val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string oris);
13.388 +
13.389 +val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt pits);
13.390 +val pits = get_obj g_pbl pt [];writeln(I_Model.to_string ctxt pits);
13.391 +
13.392 +val mits = get_obj g_met pt (fst p);writeln(I_Model.to_string ctxt mits);
13.393 +val mits = get_obj g_met pt [];writeln(I_Model.to_string ctxt mits);
13.394 +
13.395 +(*=== inhibit exn 110722=============================================================
13.396 +arguments_from_model ["Diff_App", "max_by_calculus"] mits;
13.397 +
13.398 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.399 +=== inhibit exn 110722=============================================================*)
13.400 +
13.401 +(*---*)
13.402 +
13.403 +"--------- autoCalc .. scripts for maximum-example ---------------";
13.404 +"--------- autoCalc .. scripts for maximum-example ---------------";
13.405 +"--------- autoCalc .. scripts for maximum-example ---------------";
13.406 +(*++++++++ see systest/inform.sml 'I_Model.complete' ++++++++*)
13.407 + reset_states ();
13.408 +val fmz =
13.409 + ["fixedValues [r=Arbfix]", "maximum A",
13.410 + "valuesFor [a,b]",
13.411 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
13.412 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
13.413 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
13.414 +
13.415 + "boundVariable a", "boundVariable b", "boundVariable alpha",
13.416 + "interval {x::real. 0 <= x & x <= 2*r}",
13.417 + "interval {x::real. 0 <= x & x <= 2*r}",
13.418 + "interval {x::real. 0 <= x & x <= pi}",
13.419 + "errorBound (eps=(0::real))"];
13.420 +val (dI',pI',mI') =
13.421 + ("Diff_App",["maximum_of", "function"],
13.422 + ["Diff_App", "max_by_calculus"]);
13.423 +
13.424 + CalcTree [(fmz, (dI',pI',mI'))];
13.425 + Iterator 1; moveActiveRoot 1;
13.426 + autoCalculate 1 CompleteCalcHead;
13.427 + refFormula 1 (get_pos 1 1);
13.428 +
13.429 + fetchProposedTactic 1;
13.430 +(*autoCalculate 1 (Steps 1);
13.431 + broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite
13.432 + this test is not up to date
13.433 + ERROR exception TERM raised (line 359 of "term.ML"): fastype_of: Bound B.0*)
13.434 +
13.435 + fetchProposedTactic 1;
13.436 +(*autoCalculate 1 (Steps 1);
13.437 + broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite
13.438 + this test is not up to date
13.439 + ERROR exception TERM raised (line 359 of "term.ML"): fastype_of: Bound B.0*)
13.440 + (*Subproblem on_interval maximum_of function*)
13.441 + autoCalculate 1 CompleteCalcHead;
13.442 +
13.443 + fetchProposedTactic 1;
13.444 + val ((pt,p),_) = get_calc 1;
13.445 + val mits = get_obj g_met pt (fst p);
13.446 + writeln (I_Model.to_string ctxt mits);
13.447 +(*
13.448 + if I_Model.to_string ctxt mits = "[\n(1 ,[1] ,true ,#Given ,Cor functionEq (hd r_s) ,(t_, [hd r_s])),\n(2 ,[1] ,true ,#Given ,Cor boundVariable v_v ,(v_, [v_])),\n(3 ,[1] ,true ,#Given ,Cor interval itv_ ,(itv_, [itv_])),\n(4 ,[1] ,true ,#Find ,Cor maxArgument v__0 ,(v_0, [v__0]))]" then ()
13.449 + else error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
13.450 +*)
13.451 + (*FIXME: the environments contain identifers, and NOT values ?!?!?*)
13.452 +(* WN051209 while extending 'fun step' for initac, this became better ...
13.453 + if I_Model.to_string ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(v_s, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(r_s, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then ()
13.454 + else error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
13.455 +*)
13.456 +
13.457 +
13.458 +
13.459 +"--------------------- 30.4.03: maximum .. rewrite_set_ prog_expr ---------";
13.460 +"--------------------- 30.4.03: maximum .. rewrite_set_ prog_expr ---------";
13.461 +"--------------------- 30.4.03: maximum .. rewrite_set_ prog_expr ---------";
13.462 +TermC.str2term
13.463 + "Program Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list)\
13.464 + \ (v_v::real) (itv_v::real set) (err_r::bool) = \
13.465 + \ (let e_e = (hd o (filterVar m_m)) r_s; \
13.466 + \ t_t = (if 1 < length_h r_s \
13.467 + \ then (SubProblem (Reals_s,[make,function],[no_met])\
13.468 + \ [REAL m_m, REAL v_v, BOOL_LIST r_s])\
13.469 + \ else (hd r_s)); \
13.470 + \ (mx_x::real) = SubProblem (Reals_s,[on_interval,max_of,function], \
13.471 + \ [Isac,maximum_on_interval])\
13.472 + \ [BOOL t_t, REAL v_v, REAL_SET itv_v]\
13.473 + \ in ((SubProblem (Reals_s,[find_values,tool],[Isac,find_values]) \
13.474 + \ [REAL mx_x, REAL (Rhs t_t), REAL v_v, REAL m_m, \
13.475 + \ BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list))";
13.476 +
13.477 +val f_ix = (TermC.str2term "f_ix::bool list",
13.478 + TermC.str2term "[r=Arbfix]");
13.479 +val m_m = (TermC.str2term "m_m::real",
13.480 + TermC.str2term "A");
13.481 +val r_s = (TermC.str2term "rs_s::bool list",
13.482 + TermC.str2term "[A = a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]");
13.483 +val v_v = (TermC.str2term "v_v::real",
13.484 + TermC.str2term "b");
13.485 +val itv_v = (TermC.str2term "itv_v::real set",
13.486 + TermC.str2term "{x::real. 0 <= x & x <= 2*r}");
13.487 +val err_r = (TermC.str2term "err_r::bool",
13.488 + TermC.str2term "eps=0");
13.489 +val env = [f_ix, m_m, r_s ,v_v, itv_v, err_r];
13.490 +
13.491 +(*--- 1.line in script ---*)
13.492 +val t = TermC.str2term "(hd o (filterVar m_m)) (r_s::bool list)";
13.493 +val s = subst_atomic env t;
13.494 +UnparseC.term s;
13.495 +"(hd o filterVar A) [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]";
13.496 +(*=== inhibit exn 110726=============================================================
13.497 +val SOME (s',_) = rewrite_set_ thy false prog_expr s;
13.498 +val s'' = UnparseC.term s';
13.499 +if s''="A = a * b" then () else error "new behaviour with prog_expr 1.1.";
13.500 +=== inhibit exn 110726=============================================================*)
13.501 +val env = env @ [(TermC.str2term "e_e::bool",TermC.str2term "A = a * b")];
13.502 +
13.503 +(*--- 2.line: condition alone ---*)
13.504 +val t = TermC.str2term "1 < length_h (r_s::bool list)";
13.505 +val s = subst_atomic env t;
13.506 +UnparseC.term s;
13.507 +"1 < length_h [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]";
13.508 +(*=== inhibit exn 110726=============================================================
13.509 +val SOME (s',_) = rewrite_set_ thy false prog_expr s;
13.510 +val s'' = UnparseC.term s';
13.511 +if s''=\<^const_name>\<open>True\<close> then () else error "new behaviour with prog_expr 1.2.";
13.512 +=== inhibit exn 110726=============================================================*)
13.513 +
13.514 +(*--- 2.line in script ---*)
13.515 +val t = TermC.str2term
13.516 + "(if 1 < length_h r_s \
13.517 + \ then (SubProblem (Reals_s,[make,function],[no_met])\
13.518 + \ [REAL m_m, REAL v_v, BOOL_LIST r_s])\
13.519 + \ else (hd r_s))";
13.520 +val s = subst_atomic env t;
13.521 +UnparseC.term s;
13.522 +"if 1 < length_h [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]\
13.523 +\then SubProblem (Reals_s, [make, function], [no_met])\
13.524 +\ [REAL A, REAL b,\
13.525 +\ BOOL_LIST [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]\
13.526 +\else hd [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]";
13.527 +(*=== inhibit exn 110726=============================================================
13.528 +val SOME (s',_) = rewrite_set_ thy false prog_expr s;
13.529 +val s'' = UnparseC.term s';
13.530 +if s'' =
13.531 +"SubProblem (Reals_s, [make, function], [no_met])\n\
13.532 +\ [REAL A, REAL b,\n\
13.533 +\ BOOL_LIST [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]" then ()
13.534 +else error "new behaviour with prog_expr 1.3.";
13.535 +=== inhibit exn 110726=============================================================*)
13.536 +val env = env @ [(TermC.str2term "t_t::bool",
13.537 + TermC.str2term "A = (2*sqrt(r \<up> 2-(b/2) \<up> 2)) * b")];
13.538 +
13.539 +
13.540 +
13.541 +"---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
13.542 +"---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
13.543 +"---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
13.544 +TermC.str2term
13.545 + "Program Make_fun_by_explicit (f_f::real) (v_v::real) \
13.546 + \ (eqs::bool list) = \
13.547 + \ (let h_h = (hd o (filterVar f_f)) eqs; \
13.548 + \ e_1 = hd (dropWhile (ident h_h) eqs); \
13.549 + \ v_s = dropWhile (ident f_f) (Vars h_h); \
13.550 + \ v_1 = hd (dropWhile (ident v_v) v_s); \
13.551 + \ (s_1::bool list)=(SubProblem(Reals_s,[univar,equation],[no_met])\
13.552 + \ [BOOL e_1, REAL v_1])\
13.553 + \ in Substitute [(v_1 = (rhs o hd) s_1)] h_h)";
13.554 +val f_f = (TermC.str2term "f_f::real",
13.555 + TermC.str2term "A");
13.556 +val v_v = (TermC.str2term "v_v::real",
13.557 + TermC.str2term "b");
13.558 +val eqs=(TermC.str2term "eqs::bool list",
13.559 + TermC.str2term "[A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]");
13.560 +val env = [f_f, v_v, eqs];
13.561 +
13.562 +(*--- 1.line in script ---*)
13.563 +val t = TermC.str2term "(hd o (filterVar v_v)) (eqs::bool list)";
13.564 +val s = subst_atomic env t;
13.565 +UnparseC.term s;
13.566 +val t = TermC.str2term
13.567 + "(hd o filterVar b) [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]";
13.568 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
13.569 +val s' = UnparseC.term t';
13.570 +(*=== inhibit exn 110726=============================================================
13.571 +if s' = "A = a * b" then () else error "new behaviour with prog_expr 2.1";
13.572 +=== inhibit exn 110726=============================================================*)
13.573 +val env = env @ [(TermC.str2term "h_h::bool", TermC.str2term s')];
13.574 +
13.575 +(*--- 2.line in script ---*)
13.576 +val t = TermC.str2term "hd (dropWhile (ident h_h) (eqs::bool list))";
13.577 +val s = subst_atomic env t;
13.578 +UnparseC.term s;
13.579 +val t = TermC.str2term
13.580 + "hd (dropWhile (ident (A = a * b))\
13.581 + \ [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2])";
13.582 +(*=== inhibit exn 110726=============================================================
13.583 +mem_rls "dropWhile_Cons" prog_expr;
13.584 +mem_rls "Prog_Expr.ident" prog_expr;
13.585 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
13.586 +val s' = UnparseC.term t';
13.587 +if s' = "(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2" then ()
13.588 +else error "new behaviour with prog_expr 2.2";
13.589 +=== inhibit exn 110726=============================================================*)
13.590 +val env = env @ [(TermC.str2term "e_1::bool", TermC.str2term s')];
13.591 +
13.592 +(*--- 3.line in script ---*)
13.593 +val t = TermC.str2term "dropWhile (ident f_f) (Vars (h_h::bool))";
13.594 +val s = subst_atomic env t;
13.595 +UnparseC.term s;
13.596 +val t = TermC.str2term "dropWhile (ident A) (Vars (A = a * b))";
13.597 +(*=== inhibit exn 110726=============================================================
13.598 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
13.599 +val s' = UnparseC.term t';
13.600 +if s' = "[a, b]" then () else error "new behaviour with prog_expr 2.3";
13.601 +=== inhibit exn 110726=============================================================*)
13.602 +val env = env @ [(TermC.str2term "vs_s::real list", TermC.str2term s')];
13.603 +
13.604 +(*--- 4.line in script ---*)
13.605 +val t = TermC.str2term "hd (dropWhile (ident v_v) v_s)";
13.606 +val s = subst_atomic env t;
13.607 +UnparseC.term s;
13.608 +val t = TermC.str2term "hd (dropWhile (ident b) [a, b])";
13.609 +(*=== inhibit exn 110726=============================================================
13.610 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
13.611 +val s' = UnparseC.term t';
13.612 +if s' = "a" then () else error "new behaviour with prog_expr 2.4.";
13.613 +=== inhibit exn 110726=============================================================*)
13.614 +val env = env @ [(TermC.str2term "v_1::real", TermC.str2term s')];
13.615 +
13.616 +(*--- 5.line in script ---*)
13.617 +val t = TermC.str2term "(SubProblem(Reals_s,[univar,equation],[no_met])\
13.618 + \ [BOOL e_1, REAL v_1])";
13.619 +val s = subst_atomic env t;
13.620 +UnparseC.term s;
13.621 +"SubProblem (Reals_s, [univar, equation], [no_met])\n\
13.622 +\ [BOOL ((a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2), REAL a]";
13.623 +val env = env @ [(TermC.str2term "s_1::bool list",
13.624 + TermC.str2term "[a = 2 * sqrt (r \<up> 2 - (b/2) \<up> 2)]")];
13.625 +
13.626 +(*--- 6.line in script ---*)
13.627 +val t = TermC.str2term "Substitute [(v_1 = (rhs o hd) (s_1::bool list))] (h_h::bool)";
13.628 +val s = subst_atomic env t;
13.629 +UnparseC.term s;
13.630 +val t = TermC.str2term
13.631 +"Substitute [(a = (rhs o hd) [a = 2 * sqrt (r \<up> 2 - (b / 2) \<up> 2)])]\n\
13.632 +\ (A = a * b)";
13.633 +(*=== inhibit exn 110726=============================================================
13.634 +mem_rls "Prog_Expr.rhs" prog_expr;
13.635 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
13.636 +val s' = UnparseC.term t';
13.637 +if s' = "Substitute [a = 2 * sqrt (r \<up> 2 - (b / 2) \<up> 2)] (A = a * b)"
13.638 +then () else error "new behaviour with prog_expr 2.6.";
13.639 +=== inhibit exn 110726=============================================================*)
13.640 +
13.641 +
13.642 +"---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
13.643 +"---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
13.644 +"---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
13.645 +TermC.str2term
13.646 + "Program Make_fun_by_new_variable (f_f::real) (v_v::real) \
13.647 + \ (eqs::bool list) = \
13.648 + \(let h_h = (hd o (filterVar f_f)) eqs; \
13.649 + \ es_s = dropWhile (ident h_h) eqs; \
13.650 + \ v_s = dropWhile (ident f_f) (Vars h_h); \
13.651 + \ v_1 = nth_h 1 v_s; \
13.652 + \ v_2 = nth_h 2 v_s; \
13.653 + \ e_1 = (hd o (filterVar v_1)) es_s; \
13.654 + \ e_2 = (hd o (filterVar v_2)) es_s; \
13.655 + \ (s_1::bool list) = (SubProblem (Reals_s,[univar,equation],[no_met])\
13.656 + \ [BOOL e_1, REAL v_1]);\
13.657 + \ (s_2::bool list) = (SubProblem (Reals_s,[univar,equation],[no_met])\
13.658 + \ [BOOL e_2, REAL v_2])\
13.659 + \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)";
13.660 +val f_ = (TermC.str2term "f_f::real",
13.661 + TermC.str2term "A");
13.662 +val v_v = (TermC.str2term "v_v::real",
13.663 + TermC.str2term "alpha");
13.664 +val eqs=(TermC.str2term "eqs::bool list",
13.665 + TermC.str2term "[A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]");
13.666 +val env = [f_f, v_v, eqs];
13.667 +
13.668 +(*--- 1.line in script ---*)
13.669 +val t = TermC.str2term "(hd o (filterVar (f_f::real))) (eqs::bool list)";
13.670 +val s = subst_atomic env t;
13.671 +UnparseC.term s;
13.672 +val t = TermC.str2term
13.673 +"(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
13.674 +Rewrite.trace_on := false; (*true false*)
13.675 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
13.676 +Rewrite.trace_on:=false; (*true false*)
13.677 +val s' = UnparseC.term t';
13.678 +(*=== inhibit exn 110726=============================================================
13.679 +if s' = "A = a * b" then() else error "new behaviour with prog_expr 3.1.";
13.680 +val env = env @ [(TermC.str2term "h_h::bool", TermC.str2term s')];
13.681 +=== inhibit exn 110726=============================================================*)
13.682 +
13.683 +(*--- 2.line in script ---*)
13.684 +val t = TermC.str2term "dropWhile (ident (h_h::bool)) (eqs::bool list)";
13.685 +val s = subst_atomic env t;
13.686 +UnparseC.term s;
13.687 +val t = TermC.str2term
13.688 +"dropWhile (ident (A = a * b))\
13.689 +\ [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
13.690 +(*=== inhibit exn 110726=============================================================
13.691 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
13.692 +val s' = UnparseC.term t';
13.693 +if s' = "[a / 2 = r * sin alpha, b / 2 = r * cos alpha]"
13.694 +then () else error "new behaviour with prog_expr 3.2.";
13.695 +=== inhibit exn 110726=============================================================*)
13.696 +val env = env @ [(TermC.str2term "es_s::bool list", TermC.str2term s')];
13.697 +
13.698 +(*--- 3.line in script ---*)
13.699 +val t = TermC.str2term "dropWhile (ident (f_f::real)) (Vars (h_h::bool))";
13.700 +val s = subst_atomic env t;
13.701 +UnparseC.term s;
13.702 +val t = TermC.str2term "dropWhile (ident A) (Vars (A = a * b))";
13.703 +(*=== inhibit exn 110726=============================================================
13.704 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
13.705 +val s' = UnparseC.term t';
13.706 +if s' = "[a, b]" then () else error "new behaviour with prog_expr 3.3.";
13.707 +=== inhibit exn 110726=============================================================*)
13.708 +val env = env @ [(TermC.str2term "vs_s::real list", TermC.str2term s')];
13.709 +
13.710 +(*--- 4.line in script ---*)
13.711 +val t = TermC.str2term "nth_h 1 v_s";
13.712 +val s = subst_atomic env t;
13.713 +UnparseC.term s;
13.714 +val t = TermC.str2term "nth_h 1 [a, b]";
13.715 +(*=== inhibit exn 110726=============================================================
13.716 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
13.717 +val s' = UnparseC.term t';
13.718 +if s' = "a" then () else error "new behaviour with prog_expr 3.4.";
13.719 +=== inhibit exn 110726=============================================================*)
13.720 +val env = env @ [(TermC.str2term "v_1", TermC.str2term s')];
13.721 +
13.722 +(*--- 5.line in script ---*)
13.723 +val t = TermC.str2term "nth_h 2 v_s";
13.724 +val s = subst_atomic env t;
13.725 +UnparseC.term s;
13.726 +val t = TermC.str2term "nth_h 2 [a, b]";
13.727 +(*=== inhibit exn 110726=============================================================
13.728 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
13.729 +val s' = UnparseC.term t';
13.730 +if s' = "b" then () else error "new behaviour with prog_expr 3.5.";
13.731 +=== inhibit exn 110726=============================================================*)
13.732 +val env = env @ [(TermC.str2term "v_2", TermC.str2term s')];
13.733 +
13.734 +(*--- 6.line in script ---*)
13.735 +val t = TermC.str2term "(hd o (filterVar v_1)) (es_s::bool list)";
13.736 +val s = subst_atomic env t;
13.737 +UnparseC.term s;
13.738 +val t = TermC.str2term
13.739 + "(hd o filterVar a) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
13.740 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
13.741 +val s' = UnparseC.term t';
13.742 +(*=== inhibit exn 110726=============================================================
13.743 +if s' = "a / 2 = r * sin alpha" then ()
13.744 +else error "new behaviour with prog_expr 3.6.";
13.745 +=== inhibit exn 110726=============================================================*)
13.746 +val e_1 = TermC.str2term "e_1::bool";
13.747 +val env = env @ [(e_1, TermC.str2term s')];
13.748 +
13.749 +(*--- 7.line in script ---*)
13.750 +val t = TermC.str2term "(hd o (filterVar v_2)) (es_s::bool list)";
13.751 +val s = subst_atomic env t;
13.752 +UnparseC.term s;
13.753 +val t = TermC.str2term
13.754 + "(hd o filterVar b) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
13.755 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
13.756 +val s' = UnparseC.term t';
13.757 +(*=== inhibit exn 110726=============================================================
13.758 +if s' = "b / 2 = r * cos alpha" then ()
13.759 +else error "new behaviour with prog_expr 3.7.";
13.760 +=== inhibit exn 110726=============================================================*)
13.761 +val env = env @ [(TermC.str2term "e_2::bool", TermC.str2term s')];
13.762 +
13.763 +(*--- 8.line in script ---*)
13.764 +val t = TermC.str2term "(SubProblem (Reals_s,[univar,equation],[no_met])\
13.765 + \ [BOOL e_1, REAL v_1])";
13.766 +val s = subst_atomic env t;
13.767 +UnparseC.term s;
13.768 +"SubProblem (Reals_s, [univar, equation], [no_met])\
13.769 + \ [BOOL (a / 2 = r * sin alpha), REAL a]";
13.770 +val s_1 = TermC.str2term "[a = 2*r*sin alpha]";
13.771 +val env = env @ [(TermC.str2term "s_1::bool list", s_1)];
13.772 +
13.773 +(*--- 9.line in script ---*)
13.774 +val t = TermC.str2term "(SubProblem (Reals_s,[univar,equation],[no_met])\
13.775 + \ [BOOL e_2, REAL v_2])";
13.776 +val s = subst_atomic env t;
13.777 +UnparseC.term s;
13.778 +"SubProblem (Reals_s, [univar, equation], [no_met])\
13.779 + \ [BOOL (b / 2 = r * cos alpha), REAL b]";
13.780 +val s_2 = TermC.str2term "[b = 2*r*cos alpha]";
13.781 +val env = env @ [(TermC.str2term "s_2::bool list", s_2)];
13.782 +
13.783 +(*--- 10.line in script ---*)
13.784 +val t = TermC.str2term
13.785 +"Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] (h_h::bool)";
13.786 +val s = subst_atomic env t;
13.787 +UnparseC.term s;
13.788 +"Substitute\n [(a = (rhs o hd) [a = 2 * r * sin alpha]),\
13.789 +\ (b = (rhs o hd) [b = 2 * r * cos alpha])] (A = a * b)";
13.790 +val SOME (s',_) = rewrite_set_ thy false prog_expr s;
13.791 +val s'' = UnparseC.term s';
13.792 +(*=== inhibit exn 110726=============================================================
13.793 +if s'' =
13.794 +"Substitute [a = 2 * r * sin alpha, b = 2 * r * cos alpha] (A = a * b)"
13.795 +then () else error "new behaviour with prog_expr 3.10.";
13.796 +===== inhibit exn 110722===========================================================*)
13.797 +
14.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Fri Jun 17 12:15:09 2022 +0200
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,794 +0,0 @@
14.4 -(* tests for IsacKnowledge/DiffApp
14.5 - author Walther Neuper 000301
14.6 - (c) due to copyright terms
14.7 -
14.8 - use"../smltest/IsacKnowledge/diffapp.sml";
14.9 - use"diffapp.sml";
14.10 -*)
14.11 -
14.12 -Rewrite.trace_on := false; (*true false*)
14.13 -"Contents----------------------------------------------";
14.14 -" Specify_Problem (match_itms_oris) ";
14.15 -" test specify, fmz <> [] ";
14.16 -" test specify, fmz = [] ";
14.17 -" problemtypes + formalizations ";
14.18 -"-------------------- ctree of {(a,b). is-max ... ----------------";
14.19 -"--------- me .. scripts for maximum-example ---------------------";
14.20 -"--------- autoCalc .. scripts for maximum-example ---------------";
14.21 -
14.22 -"--------------------- 30.4.03: maximum .. rewrite_set_ prog_expr ---------";
14.23 -"---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
14.24 -"---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
14.25 -
14.26 -
14.27 -
14.28 -
14.29 -
14.30 -" #################################################### ";
14.31 -" problemtypes + formalizations ";
14.32 -" #################################################### ";
14.33 -" -------------- [maximum_of,function] --------------- ";
14.34 -val pbt =
14.35 - ["fixedValues f_ix", "maximum m_m", "valuesFor v_s", "relations r_s"];
14.36 -(*=== inhibit exn 110722=============================================================
14.37 -map (the o (parseold thy)) pbt;
14.38 -=== inhibit exn 110722=============================================================*)
14.39 -val fmz =
14.40 - ["fixedValues [r=Arbfix]", "maximum A",
14.41 - "valuesFor [a,b]",
14.42 - "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
14.43 - "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
14.44 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
14.45 -
14.46 - "boundVariable a", "boundVariable b", "boundVariable alpha",
14.47 - "interval {x::real. 0 <= x & x <= 2*r}",
14.48 - "interval {x::real. 0 <= x & x <= 2*r}",
14.49 - "interval {x::real. 0 <= x & x <= pi}",
14.50 - "errorBound (eps=(0::real))"];
14.51 -(*=== inhibit exn 110722=============================================================
14.52 -map (the o (parseold thy)) fmz;
14.53 -" -------------- [make,function] -------------- ";
14.54 -=== inhibit exn 110722=============================================================*)
14.55 -val pbt =
14.56 - ["functionOf f_f", "boundVariable v_v", "equalities eqs",
14.57 - "functionTerm f_0_0"];
14.58 -(*=== inhibit exn 110722=============================================================
14.59 -map (the o (parseold thy)) pbt;
14.60 -val fmz12 =
14.61 - ["functionOf A", "boundVariable a", "boundVariable b",
14.62 - "equalities [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
14.63 - (*28.11.00: "functionTerm (A_0=Undef)"*)"functionTerm (Undef)"];
14.64 -map (the o (parseold thy)) fmz12;
14.65 -val fmz3 =
14.66 - ["functionOf A", "boundVariable a", "boundVariable b",
14.67 - "equalities [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
14.68 - (*28.11.00: "functionTerm (A_0=Undef)"*)"functionTerm (Undef)"];
14.69 -map (the o (parseold thy)) fmz3;
14.70 -" --------- [univar,equation] --------- ";
14.71 -val pbt =
14.72 - ["equality e_e", "solveFor v_v", "solutions v_i_i"];
14.73 -map (the o (parseold thy)) pbt;
14.74 -val fmz =
14.75 - ["equality ((a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2)",
14.76 - "solveFor b", "solutions b_i"];
14.77 -map (the o (parseold thy)) fmz;
14.78 -" ---- [on_interval,maximum_of,function] ---- ";
14.79 -val pbt =
14.80 - ["functionTerm t_t", "boundVariable v_v", "interval itv_v",
14.81 - "errorBound err_r", "maxArgument v_0"];
14.82 -map (the o (parseold thy)) pbt;
14.83 -val fmz12 =
14.84 - [(*28.11.00: "functionTerm (A_0 = a*sqrt(#4*r \<up> #2 - a \<up> #2))",*)
14.85 - "functionTerm (a*sqrt(4*r \<up> 2 - a \<up> 2))",
14.86 - (*28.11.00: "functionTerm (A_0 = b*sqrt(#4*r \<up> #2 - b \<up> #2))",*)
14.87 - "functionTerm (b*sqrt(4*r \<up> 2 - b \<up> 2))",
14.88 - "boundVariable a", "boundVariable b",
14.89 - "interval {x::real. 0 <= x & x <= 2*r}",
14.90 - "errorBound (eps=0)", "maxArgument (a_0=Undef)"];
14.91 -map (the o (parseold thy)) fmz12;
14.92 -val fmz3 =
14.93 - [(*28.11.00: "functionTerm (A_0 = (#2*r*sin alpha)*(#2*r*cos alpha))",*)
14.94 - "functionTerm ((2*r*sin alpha)*(2*r*cos alpha))",
14.95 - "boundVariable alpha",
14.96 - "interval {x::real. 0 <= x & x <= pi}",
14.97 - "errorBound (eps=0)", "maxArgument (a_0=Undef)"];
14.98 -map (the o (parseold thy)) fmz3;
14.99 -" --------- [derivative_of,function] --------- ";
14.100 -val pbt =
14.101 - ["functionTerm f_f", "boundVariable v_v", "derivative f_f'"];
14.102 -map (the o (parseold thy)) pbt;
14.103 -val fmz =
14.104 - [(*28.11.00: "functionTerm (A_0=a*#2*sqrt r \<up> #2 - (a//#2) \<up> #2)",*)
14.105 - "functionTerm (a*2*sqrt r \<up> 2 - (a/2) \<up> 2)",
14.106 - "boundVariable a",
14.107 - (*28.11.00: "derivative (A_0'=Undef)"*)"derivative (Undef)"];
14.108 -map (the o (parseold thy)) fmz;
14.109 -" --------- [find_values,tool] --------- ";
14.110 -val pbt =
14.111 - ["maxArgument ma_a", "functionTerm f_f", "boundVariable v_v",
14.112 - "valuesFor vls_s", "additionalRels r_s"];
14.113 -map (the o (parseold thy)) pbt;
14.114 -val fmz1 =
14.115 - ["maxArgument (a_0=(srqt 2)*r)",
14.116 - (*28.11.00: "functionTerm (A_0=a*#2*sqrt r \<up> #2 - (a//#2) \<up> #2)",*)
14.117 - "functionTerm (a*2*sqrt r \<up> 2 - (a/2) \<up> 2)",
14.118 - "boundVariable a",
14.119 - "valuesFor [a,b]", "maximum A",
14.120 - "additionalRels [(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"];
14.121 -map (the o (parseold thy)) fmz1;
14.122 -
14.123 -=== inhibit exn 110722=============================================================*)
14.124 -
14.125 -
14.126 -"-------------------- ctree of {(a,b). is-max ... --------------------------";
14.127 -"-------------------- ctree of {(a,b). is-max ... --------------------------";
14.128 -"-------------------- ctree of {(a,b). is-max ... --------------------------";
14.129 -
14.130 -(* --vvv-- ausgeliehen von test-root-equ/sml *)
14.131 -val loc = Istate.empty;
14.132 -val (dI',pI',mI') =
14.133 - ("Program",["sqroot-test", "univariate", "equation"],
14.134 - ["Program", "squ-equ-test2"]);
14.135 -val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
14.136 - "solveFor x", "errorBound (eps=0)",
14.137 - "solutions L"];
14.138 -(*
14.139 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
14.140 -val ((p,p_),_,_,_,_,(_,pt,_)) = CalcTreeTEST [fmz, (dI',pI',mI')))];
14.141 - -- \<up> -- ausgeliehen von test-root-equ/sml *)
14.142 -(*-------------- 9.6.03 --- cappend_ ... term -------irreparabler test
14.143 -val (pt,_) =
14.144 - cappend_problem EmptyPtree [] loc ([],(dI',pI',mI'), .....);
14.145 -val pos = (lev_on o lev_dn) [];
14.146 -(* val pos = ([1]) *)
14.147 -val (pt,_) = cappend_parent pt pos loc "{(a,b). is-max ..."
14.148 - Empty_Tac TransitiveB;
14.149 -val pos = (lev_on o lev_dn) pos;
14.150 -(*val pos = ([1,1])*)
14.151 -val (pt,_) = cappend_atomic pt pos loc "{(a,b). is-max ..."
14.152 - Empty_Tac ("[1,1]:{(a,b). is-extremum ...",[]) Complete;
14.153 -val pos = lev_on pos;
14.154 -(*val pos = ([1,2])*)
14.155 -val (pt,_) = cappend_atomic pt pos loc "{(a,b). is-extremum ..."
14.156 - Empty_Tac ("[1,2]:{(a,b). f_x(a,b) ...",[]) Complete;
14.157 -val pos = lev_up pos;
14.158 -(*val pos = ([1])*)
14.159 -val (pt,_) = append_result pt pos Istate.empty ("[1#]:{(a,b). f_x(a,b) ...",[])
14.160 - Complete;
14.161 -
14.162 -val pos = lev_on pos;
14.163 -(*val pos = ([2]) *)
14.164 -val (pt,_) = cappend_atomic pt pos loc "{(a,b). f_x(a,b) ..."
14.165 - Empty_Tac ("[2]:{(a,b). f_x & f_xx &...",[]) Complete;
14.166 -val pos = lev_on pos;
14.167 -(*al pos = [3] : pos*)
14.168 -val (pt,_) = cappend_parent pt pos loc "{(a,b). f_x & f_xx &..."
14.169 - Empty_Tac TransitiveB;
14.170 -val pos = (lev_on o lev_dn) pos;
14.171 -(*pos = ([3,1]) *)
14.172 -val (pt,_) = cappend_atomic pt pos loc "{(a,b). f_x & f_xx & ..."
14.173 - Empty_Tac ("[3,1]:{(a,b). f_x & f_xx } cup ...",[]) Complete;
14.174 -val pos = lev_on pos;
14.175 -(*pos = ([3,2]) *)
14.176 -val (pt,_) = cappend_atomic pt pos loc "{(a,b). f_x & f_xx } cup.."
14.177 - Empty_Tac ("[3,2]:{(a,b). f_x ..} cup ...",[]) Complete;
14.178 -
14.179 -val pos = lev_up pos;
14.180 -(*pos = ([3]) *)
14.181 -val (pt,_) = append_result pt pos Istate.empty ("[3#]:{(a,b). f_x ..} cup..",[])
14.182 - Complete;
14.183 -val pos = lev_on pos;
14.184 -(*val pos = [4] : pos *)
14.185 -val (pt,_) = cappend_parent pt pos loc "{(a,b). f_x ..} cup ..."
14.186 - Empty_Tac IntersectB;
14.187 -val pos = (lev_on o lev_dn) pos;
14.188 -(*val pos = ([4,1]) *)
14.189 -val (pt,_) = cappend_parent pt pos loc "set_1 = ..."
14.190 - Empty_Tac SequenceB;
14.191 -
14.192 -
14.193 -val pos = (lev_on o lev_dn) pos;
14.194 -(*val pos = ([4,1,1]) *)
14.195 -val (pt,_) = cappend_parent(*pbl*) pt pos loc"f_x = d/dx x \<up> 3 ..."
14.196 - Empty_Tac TransitiveB;
14.197 -val pos = (lev_on o lev_dn) pos;
14.198 -(*val pos = ([4,1,1,1]) *)
14.199 -val (pt,_) = cappend_parent pt pos loc "d/dx x \<up> 3 ..."
14.200 - Empty_Tac TransitiveB;
14.201 -val pos = (lev_on o lev_dn) pos;
14.202 -(*val pos = ([4,1,1,1,1]) *)
14.203 -val (pt,_) = cappend_atomic pt pos loc "d/dx x \<up> 3 ..."
14.204 - Empty_Tac ("[4,1,1,1,1]:3x \<up> 2 + d/dx ...",[]) Complete;
14.205 -val pos = lev_on pos;
14.206 -(*val pos = ([4,1,1,1,2]) *)
14.207 -val (pt,_) = cappend_atomic pt pos loc "3x \<up> 2 + d/dx ..."
14.208 - Empty_Tac ("[4,1,1,1,2]:3x \<up> 2 + 0 + d/dx ...",[]) Complete;
14.209 -val pos = lev_on pos;
14.210 -(*pos = ([4,1,1,1,3]) *)
14.211 -val (pt,_) = cappend_atomic pt pos loc "3x \<up> 2 + 0 + d/dx ..."
14.212 - Empty_Tac ("[4,1,1,1,3]:3x \<up> 2 + 0 -3 ...",[]) Complete;
14.213 -"--- 1 ---";
14.214 -val pos = lev_up pos;
14.215 -(*pos = ([4,1,1,1]) *)
14.216 -val (pt,_) = append_result pt pos Istate.empty ("[4,1,1,1#]:3x \<up> 2 -3.",[])Complete;
14.217 -"--- 2 ---";
14.218 -val pos = lev_up pos;
14.219 -(*val pos = ([4,1,1]) *)
14.220 -val (pt,_) = append_result pt pos Istate.empty ("[4,1,1#]:found 3x \<up> 2 -3 ...",[])
14.221 - Complete;
14.222 -"--- 3 ---";
14.223 -val pos = lev_on pos;
14.224 -(*val pos = ([4,1,2]+) *)
14.225 -val (pt,_) = cappend_parent(*pbl*) pt pos loc "f_y = d/dy x \<up> 3 ..."
14.226 - Empty_Tac TransitiveB;
14.227 -"--- 4 ---";
14.228 -writeln (pr_ctree pr_short pt);
14.229 -
14.230 -(*
14.231 -. ----- pblobj -----
14.232 -1. {(a,b). is-max ...
14.233 -1.1. {(a,b). is-max ...
14.234 -1.2. {(a,b). is-extremum ...
14.235 -2. {(a,b). f_x(a,b) ...
14.236 -3. {(a,b). f_x & f_xx &...
14.237 -3.1. {(a,b). f_x & f_xx & ...
14.238 -3.2. {(a,b). f_x & f_xx } cup..
14.239 -4. {(a,b). f_x ..} cup ...
14.240 -4.1. set_1 = ...
14.241 -4.1.1. f_x = d/dx x \<up> 3 ...
14.242 -4.1.1.1. d/dx x \<up> 3 ...
14.243 -4.1.1.1.1. d/dx x \<up> 3 ...
14.244 -4.1.1.1.2. 3x \<up> 2 + d/dx ...
14.245 -4.1.1.1.3. 3x \<up> 2 + 0 + d/dx ...
14.246 -4.1.2. f_y = d/dy x \<up> 3 ...
14.247 -
14.248 - use"test-max-surf1.sml";
14.249 - *)
14.250 --------------- 9.6.03 --- cappend_ ... term -------irreparabler test---*)
14.251 -
14.252 -
14.253 -"--------- me .. scripts for maximum-example ---------------------";
14.254 -"--------- me .. scripts for maximum-example ---------------------";
14.255 -"--------- me .. scripts for maximum-example ---------------------";
14.256 -
14.257 -val fmz =
14.258 - ["fixedValues [r=Arbfix]", "maximum A",
14.259 - "valuesFor [a,b]",
14.260 - "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
14.261 - "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
14.262 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
14.263 -
14.264 - "boundVariable a", "boundVariable b", "boundVariable alpha",
14.265 - "interval {x::real. 0 <= x & x <= 2*r}",
14.266 - "interval {x::real. 0 <= x & x <= 2*r}",
14.267 - "interval {x::real. 0 <= x & x <= pi}",
14.268 - "errorBound (eps=(0::real))"];
14.269 -val (dI',pI',mI') =
14.270 - ("DiffApp",["maximum_of", "function"],
14.271 - ["DiffApp", "max_by_calculus"]);
14.272 -
14.273 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
14.274 -(*=== inhibit exn 110722=============================================================
14.275 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.276 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.277 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.278 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.279 -val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
14.280 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.281 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.282 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.283 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.284 -case nxt of (_, Specify_Method ["DiffApp", "max_by_calculus"]) => ()
14.285 - | _ => error "diffapp.sml: max-exp me, nxt = Specify_Method";
14.286 -
14.287 -val oris = fst3 (get_obj g_origin pt (fst p)); writeln(O_Model.to_string oris);
14.288 -val pits = get_obj g_pbl pt (fst p); writeln(I_Model.to_string ctxt pits);
14.289 -
14.290 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.291 -val mits = get_obj g_met pt (fst p); writeln(I_Model.to_string ctxt mits);
14.292 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.293 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.294 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.295 -case nxt of (_,Apply_Method ["DiffApp", "max_by_calculus"] ) => ()
14.296 - | _ => error "diffapp.sml: max-exp me, nxt = Apply_Method";
14.297 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.298 -=== inhibit exn 110722=============================================================*)
14.299 -
14.300 -(*since 0508 Apply_Method does the 1st step, if NONE implicit_take -------------
14.301 -(*val nxt = ("Subproblem",Subproblem ("DiffApp",["make", "function"]))*)
14.302 -val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn_G e;
14.303 -(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["make", "function"])*)
14.304 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.305 -(*val nxt = ("Model_Problem",Model_Problem ["by_explicit", "make", "function"])*)
14.306 -----------------------------------------------------------------------------*)
14.307 -case nxt of (Model_Problem(*["by_explicit", "make", "function"]*)) => ()
14.308 - | _ => error "diffapp.sml: max-exp me, nxt = Model_Problem";
14.309 -
14.310 -(*=== inhibit exn 110722=============================================================
14.311 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.312 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.313 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.314 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.315 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.316 -=== inhibit exn 110722=============================================================*)
14.317 -
14.318 -val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string oris);
14.319 -val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt pits);
14.320 -
14.321 -(*=== inhibit exn 110722=============================================================
14.322 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.323 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.324 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.325 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.326 -case nxt of (_, Apply_Method ["DiffApp", "make_fun_by_explicit"]) => ()
14.327 - | _ => error "diffapp.sml: max-exp Apply_Method ([1], Met) ";
14.328 -=== inhibit exn 110722=============================================================*)
14.329 -
14.330 -(*----since WN050901 (ie. corr. mathengine#nxt_specify_ ..Specify.find_next_step' Pbl->p_
14.331 -we get at ...
14.332 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.333 -...
14.334 -### associate: Not_Associated m= Subproblem' ,
14.335 - stac= Substitute
14.336 - [(b, (rhs o hd)
14.337 - (Subproblem (thy, [normalise, polynomial, univariate, equation])))]
14.338 - (hd (filterVar A [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]))
14.339 -*** tac_from_prog TODO: no match for Substitute
14.340 -*** [(b, (rhs o hd)
14.341 -*** (Subproblem (thy, [normalise, polynomial, univariate, equation])))]
14.342 -*** (hd (filterVar A [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]))
14.343 -Exception- ERROR raised
14.344 -
14.345 -############################################################################
14.346 -# presumerably didnt work before either, but not detected due to Emtpy_Tac #
14.347 -############################################################################
14.348 -
14.349 -(*val nxt = Subproblem ("DiffApp",["univariate", "equation"])) *)
14.350 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.351 -(*val nxt = Refine_Tacitly ["univariate", "equation"])*)
14.352 -
14.353 -val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string oris);
14.354 -val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt pits);
14.355 -
14.356 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.357 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.358 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.359 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.360 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.361 -(*val nxt = ("Apply_Method",Apply_Method ["PolyEq", "normalise_poly"])*)
14.362 -
14.363 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.364 -(*val f = Form' (Test_Out.FormKF (~1,EdUndef,3,Nundef,"A = a * b"))*)
14.365 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.366 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.367 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.368 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.369 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.370 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.371 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.372 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.373 -(*val f = Form' (Test_Out.FormKF (~1,EdUndef,4,Nundef,"[b = A / a]"))*)
14.374 -
14.375 -------------------------------------------------------------------------*)
14.376 -
14.377 -(*val f =
14.378 -Error' (Error_ "Refine_Tacitly [\"univariate\",\"equation\"] not applicable")*)
14.379 -
14.380 -
14.381 -(*----postponed.15.5.03 run scripts for maximum-example: univariate equation*)
14.382 -(*=== inhibit exn 110722=============================================================
14.383 -
14.384 -val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
14.385 -=== inhibit exn 110722=============================================================*)
14.386 -
14.387 -val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string oris);
14.388 -
14.389 -val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt pits);
14.390 -val pits = get_obj g_pbl pt [];writeln(I_Model.to_string ctxt pits);
14.391 -
14.392 -val mits = get_obj g_met pt (fst p);writeln(I_Model.to_string ctxt mits);
14.393 -val mits = get_obj g_met pt [];writeln(I_Model.to_string ctxt mits);
14.394 -
14.395 -(*=== inhibit exn 110722=============================================================
14.396 -arguments_from_model ["DiffApp", "max_by_calculus"] mits;
14.397 -
14.398 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.399 -=== inhibit exn 110722=============================================================*)
14.400 -
14.401 -(*---*)
14.402 -
14.403 -"--------- autoCalc .. scripts for maximum-example ---------------";
14.404 -"--------- autoCalc .. scripts for maximum-example ---------------";
14.405 -"--------- autoCalc .. scripts for maximum-example ---------------";
14.406 -(*++++++++ see systest/inform.sml 'I_Model.complete' ++++++++*)
14.407 - reset_states ();
14.408 -val fmz =
14.409 - ["fixedValues [r=Arbfix]", "maximum A",
14.410 - "valuesFor [a,b]",
14.411 - "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
14.412 - "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
14.413 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
14.414 -
14.415 - "boundVariable a", "boundVariable b", "boundVariable alpha",
14.416 - "interval {x::real. 0 <= x & x <= 2*r}",
14.417 - "interval {x::real. 0 <= x & x <= 2*r}",
14.418 - "interval {x::real. 0 <= x & x <= pi}",
14.419 - "errorBound (eps=(0::real))"];
14.420 -val (dI',pI',mI') =
14.421 - ("DiffApp",["maximum_of", "function"],
14.422 - ["DiffApp", "max_by_calculus"]);
14.423 -
14.424 - CalcTree [(fmz, (dI',pI',mI'))];
14.425 - Iterator 1; moveActiveRoot 1;
14.426 - autoCalculate 1 CompleteCalcHead;
14.427 - refFormula 1 (get_pos 1 1);
14.428 -
14.429 - fetchProposedTactic 1;
14.430 -(*autoCalculate 1 (Steps 1);
14.431 - broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite
14.432 - this test is not up to date
14.433 - ERROR exception TERM raised (line 359 of "term.ML"): fastype_of: Bound B.0*)
14.434 -
14.435 - fetchProposedTactic 1;
14.436 -(*autoCalculate 1 (Steps 1);
14.437 - broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite
14.438 - this test is not up to date
14.439 - ERROR exception TERM raised (line 359 of "term.ML"): fastype_of: Bound B.0*)
14.440 - (*Subproblem on_interval maximum_of function*)
14.441 - autoCalculate 1 CompleteCalcHead;
14.442 -
14.443 - fetchProposedTactic 1;
14.444 - val ((pt,p),_) = get_calc 1;
14.445 - val mits = get_obj g_met pt (fst p);
14.446 - writeln (I_Model.to_string ctxt mits);
14.447 -(*
14.448 - if I_Model.to_string ctxt mits = "[\n(1 ,[1] ,true ,#Given ,Cor functionEq (hd r_s) ,(t_, [hd r_s])),\n(2 ,[1] ,true ,#Given ,Cor boundVariable v_v ,(v_, [v_])),\n(3 ,[1] ,true ,#Given ,Cor interval itv_ ,(itv_, [itv_])),\n(4 ,[1] ,true ,#Find ,Cor maxArgument v__0 ,(v_0, [v__0]))]" then ()
14.449 - else error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
14.450 -*)
14.451 - (*FIXME: the environments contain identifers, and NOT values ?!?!?*)
14.452 -(* WN051209 while extending 'fun step' for initac, this became better ...
14.453 - if I_Model.to_string ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(v_s, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(r_s, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then ()
14.454 - else error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
14.455 -*)
14.456 -
14.457 -
14.458 -
14.459 -"--------------------- 30.4.03: maximum .. rewrite_set_ prog_expr ---------";
14.460 -"--------------------- 30.4.03: maximum .. rewrite_set_ prog_expr ---------";
14.461 -"--------------------- 30.4.03: maximum .. rewrite_set_ prog_expr ---------";
14.462 -TermC.str2term
14.463 - "Program Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list)\
14.464 - \ (v_v::real) (itv_v::real set) (err_r::bool) = \
14.465 - \ (let e_e = (hd o (filterVar m_m)) r_s; \
14.466 - \ t_t = (if 1 < length_h r_s \
14.467 - \ then (SubProblem (Reals_s,[make,function],[no_met])\
14.468 - \ [REAL m_m, REAL v_v, BOOL_LIST r_s])\
14.469 - \ else (hd r_s)); \
14.470 - \ (mx_x::real) = SubProblem (Reals_s,[on_interval,max_of,function], \
14.471 - \ [Isac,maximum_on_interval])\
14.472 - \ [BOOL t_t, REAL v_v, REAL_SET itv_v]\
14.473 - \ in ((SubProblem (Reals_s,[find_values,tool],[Isac,find_values]) \
14.474 - \ [REAL mx_x, REAL (Rhs t_t), REAL v_v, REAL m_m, \
14.475 - \ BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list))";
14.476 -
14.477 -val f_ix = (TermC.str2term "f_ix::bool list",
14.478 - TermC.str2term "[r=Arbfix]");
14.479 -val m_m = (TermC.str2term "m_m::real",
14.480 - TermC.str2term "A");
14.481 -val r_s = (TermC.str2term "rs_s::bool list",
14.482 - TermC.str2term "[A = a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]");
14.483 -val v_v = (TermC.str2term "v_v::real",
14.484 - TermC.str2term "b");
14.485 -val itv_v = (TermC.str2term "itv_v::real set",
14.486 - TermC.str2term "{x::real. 0 <= x & x <= 2*r}");
14.487 -val err_r = (TermC.str2term "err_r::bool",
14.488 - TermC.str2term "eps=0");
14.489 -val env = [f_ix, m_m, r_s ,v_v, itv_v, err_r];
14.490 -
14.491 -(*--- 1.line in script ---*)
14.492 -val t = TermC.str2term "(hd o (filterVar m_m)) (r_s::bool list)";
14.493 -val s = subst_atomic env t;
14.494 -UnparseC.term s;
14.495 -"(hd o filterVar A) [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]";
14.496 -(*=== inhibit exn 110726=============================================================
14.497 -val SOME (s',_) = rewrite_set_ thy false prog_expr s;
14.498 -val s'' = UnparseC.term s';
14.499 -if s''="A = a * b" then () else error "new behaviour with prog_expr 1.1.";
14.500 -=== inhibit exn 110726=============================================================*)
14.501 -val env = env @ [(TermC.str2term "e_e::bool",TermC.str2term "A = a * b")];
14.502 -
14.503 -(*--- 2.line: condition alone ---*)
14.504 -val t = TermC.str2term "1 < length_h (r_s::bool list)";
14.505 -val s = subst_atomic env t;
14.506 -UnparseC.term s;
14.507 -"1 < length_h [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]";
14.508 -(*=== inhibit exn 110726=============================================================
14.509 -val SOME (s',_) = rewrite_set_ thy false prog_expr s;
14.510 -val s'' = UnparseC.term s';
14.511 -if s''=\<^const_name>\<open>True\<close> then () else error "new behaviour with prog_expr 1.2.";
14.512 -=== inhibit exn 110726=============================================================*)
14.513 -
14.514 -(*--- 2.line in script ---*)
14.515 -val t = TermC.str2term
14.516 - "(if 1 < length_h r_s \
14.517 - \ then (SubProblem (Reals_s,[make,function],[no_met])\
14.518 - \ [REAL m_m, REAL v_v, BOOL_LIST r_s])\
14.519 - \ else (hd r_s))";
14.520 -val s = subst_atomic env t;
14.521 -UnparseC.term s;
14.522 -"if 1 < length_h [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]\
14.523 -\then SubProblem (Reals_s, [make, function], [no_met])\
14.524 -\ [REAL A, REAL b,\
14.525 -\ BOOL_LIST [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]\
14.526 -\else hd [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]";
14.527 -(*=== inhibit exn 110726=============================================================
14.528 -val SOME (s',_) = rewrite_set_ thy false prog_expr s;
14.529 -val s'' = UnparseC.term s';
14.530 -if s'' =
14.531 -"SubProblem (Reals_s, [make, function], [no_met])\n\
14.532 -\ [REAL A, REAL b,\n\
14.533 -\ BOOL_LIST [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]" then ()
14.534 -else error "new behaviour with prog_expr 1.3.";
14.535 -=== inhibit exn 110726=============================================================*)
14.536 -val env = env @ [(TermC.str2term "t_t::bool",
14.537 - TermC.str2term "A = (2*sqrt(r \<up> 2-(b/2) \<up> 2)) * b")];
14.538 -
14.539 -
14.540 -
14.541 -"---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
14.542 -"---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
14.543 -"---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
14.544 -TermC.str2term
14.545 - "Program Make_fun_by_explicit (f_f::real) (v_v::real) \
14.546 - \ (eqs::bool list) = \
14.547 - \ (let h_h = (hd o (filterVar f_f)) eqs; \
14.548 - \ e_1 = hd (dropWhile (ident h_h) eqs); \
14.549 - \ v_s = dropWhile (ident f_f) (Vars h_h); \
14.550 - \ v_1 = hd (dropWhile (ident v_v) v_s); \
14.551 - \ (s_1::bool list)=(SubProblem(Reals_s,[univar,equation],[no_met])\
14.552 - \ [BOOL e_1, REAL v_1])\
14.553 - \ in Substitute [(v_1 = (rhs o hd) s_1)] h_h)";
14.554 -val f_f = (TermC.str2term "f_f::real",
14.555 - TermC.str2term "A");
14.556 -val v_v = (TermC.str2term "v_v::real",
14.557 - TermC.str2term "b");
14.558 -val eqs=(TermC.str2term "eqs::bool list",
14.559 - TermC.str2term "[A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]");
14.560 -val env = [f_f, v_v, eqs];
14.561 -
14.562 -(*--- 1.line in script ---*)
14.563 -val t = TermC.str2term "(hd o (filterVar v_v)) (eqs::bool list)";
14.564 -val s = subst_atomic env t;
14.565 -UnparseC.term s;
14.566 -val t = TermC.str2term
14.567 - "(hd o filterVar b) [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]";
14.568 -val SOME (t',_) = rewrite_set_ thy false prog_expr t;
14.569 -val s' = UnparseC.term t';
14.570 -(*=== inhibit exn 110726=============================================================
14.571 -if s' = "A = a * b" then () else error "new behaviour with prog_expr 2.1";
14.572 -=== inhibit exn 110726=============================================================*)
14.573 -val env = env @ [(TermC.str2term "h_h::bool", TermC.str2term s')];
14.574 -
14.575 -(*--- 2.line in script ---*)
14.576 -val t = TermC.str2term "hd (dropWhile (ident h_h) (eqs::bool list))";
14.577 -val s = subst_atomic env t;
14.578 -UnparseC.term s;
14.579 -val t = TermC.str2term
14.580 - "hd (dropWhile (ident (A = a * b))\
14.581 - \ [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2])";
14.582 -(*=== inhibit exn 110726=============================================================
14.583 -mem_rls "dropWhile_Cons" prog_expr;
14.584 -mem_rls "Prog_Expr.ident" prog_expr;
14.585 -val SOME (t',_) = rewrite_set_ thy false prog_expr t;
14.586 -val s' = UnparseC.term t';
14.587 -if s' = "(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2" then ()
14.588 -else error "new behaviour with prog_expr 2.2";
14.589 -=== inhibit exn 110726=============================================================*)
14.590 -val env = env @ [(TermC.str2term "e_1::bool", TermC.str2term s')];
14.591 -
14.592 -(*--- 3.line in script ---*)
14.593 -val t = TermC.str2term "dropWhile (ident f_f) (Vars (h_h::bool))";
14.594 -val s = subst_atomic env t;
14.595 -UnparseC.term s;
14.596 -val t = TermC.str2term "dropWhile (ident A) (Vars (A = a * b))";
14.597 -(*=== inhibit exn 110726=============================================================
14.598 -val SOME (t',_) = rewrite_set_ thy false prog_expr t;
14.599 -val s' = UnparseC.term t';
14.600 -if s' = "[a, b]" then () else error "new behaviour with prog_expr 2.3";
14.601 -=== inhibit exn 110726=============================================================*)
14.602 -val env = env @ [(TermC.str2term "vs_s::real list", TermC.str2term s')];
14.603 -
14.604 -(*--- 4.line in script ---*)
14.605 -val t = TermC.str2term "hd (dropWhile (ident v_v) v_s)";
14.606 -val s = subst_atomic env t;
14.607 -UnparseC.term s;
14.608 -val t = TermC.str2term "hd (dropWhile (ident b) [a, b])";
14.609 -(*=== inhibit exn 110726=============================================================
14.610 -val SOME (t',_) = rewrite_set_ thy false prog_expr t;
14.611 -val s' = UnparseC.term t';
14.612 -if s' = "a" then () else error "new behaviour with prog_expr 2.4.";
14.613 -=== inhibit exn 110726=============================================================*)
14.614 -val env = env @ [(TermC.str2term "v_1::real", TermC.str2term s')];
14.615 -
14.616 -(*--- 5.line in script ---*)
14.617 -val t = TermC.str2term "(SubProblem(Reals_s,[univar,equation],[no_met])\
14.618 - \ [BOOL e_1, REAL v_1])";
14.619 -val s = subst_atomic env t;
14.620 -UnparseC.term s;
14.621 -"SubProblem (Reals_s, [univar, equation], [no_met])\n\
14.622 -\ [BOOL ((a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2), REAL a]";
14.623 -val env = env @ [(TermC.str2term "s_1::bool list",
14.624 - TermC.str2term "[a = 2 * sqrt (r \<up> 2 - (b/2) \<up> 2)]")];
14.625 -
14.626 -(*--- 6.line in script ---*)
14.627 -val t = TermC.str2term "Substitute [(v_1 = (rhs o hd) (s_1::bool list))] (h_h::bool)";
14.628 -val s = subst_atomic env t;
14.629 -UnparseC.term s;
14.630 -val t = TermC.str2term
14.631 -"Substitute [(a = (rhs o hd) [a = 2 * sqrt (r \<up> 2 - (b / 2) \<up> 2)])]\n\
14.632 -\ (A = a * b)";
14.633 -(*=== inhibit exn 110726=============================================================
14.634 -mem_rls "Prog_Expr.rhs" prog_expr;
14.635 -val SOME (t',_) = rewrite_set_ thy false prog_expr t;
14.636 -val s' = UnparseC.term t';
14.637 -if s' = "Substitute [a = 2 * sqrt (r \<up> 2 - (b / 2) \<up> 2)] (A = a * b)"
14.638 -then () else error "new behaviour with prog_expr 2.6.";
14.639 -=== inhibit exn 110726=============================================================*)
14.640 -
14.641 -
14.642 -"---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
14.643 -"---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
14.644 -"---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
14.645 -TermC.str2term
14.646 - "Program Make_fun_by_new_variable (f_f::real) (v_v::real) \
14.647 - \ (eqs::bool list) = \
14.648 - \(let h_h = (hd o (filterVar f_f)) eqs; \
14.649 - \ es_s = dropWhile (ident h_h) eqs; \
14.650 - \ v_s = dropWhile (ident f_f) (Vars h_h); \
14.651 - \ v_1 = nth_h 1 v_s; \
14.652 - \ v_2 = nth_h 2 v_s; \
14.653 - \ e_1 = (hd o (filterVar v_1)) es_s; \
14.654 - \ e_2 = (hd o (filterVar v_2)) es_s; \
14.655 - \ (s_1::bool list) = (SubProblem (Reals_s,[univar,equation],[no_met])\
14.656 - \ [BOOL e_1, REAL v_1]);\
14.657 - \ (s_2::bool list) = (SubProblem (Reals_s,[univar,equation],[no_met])\
14.658 - \ [BOOL e_2, REAL v_2])\
14.659 - \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)";
14.660 -val f_ = (TermC.str2term "f_f::real",
14.661 - TermC.str2term "A");
14.662 -val v_v = (TermC.str2term "v_v::real",
14.663 - TermC.str2term "alpha");
14.664 -val eqs=(TermC.str2term "eqs::bool list",
14.665 - TermC.str2term "[A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]");
14.666 -val env = [f_f, v_v, eqs];
14.667 -
14.668 -(*--- 1.line in script ---*)
14.669 -val t = TermC.str2term "(hd o (filterVar (f_f::real))) (eqs::bool list)";
14.670 -val s = subst_atomic env t;
14.671 -UnparseC.term s;
14.672 -val t = TermC.str2term
14.673 -"(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
14.674 -Rewrite.trace_on := false; (*true false*)
14.675 -val SOME (t',_) = rewrite_set_ thy false prog_expr t;
14.676 -Rewrite.trace_on:=false; (*true false*)
14.677 -val s' = UnparseC.term t';
14.678 -(*=== inhibit exn 110726=============================================================
14.679 -if s' = "A = a * b" then() else error "new behaviour with prog_expr 3.1.";
14.680 -val env = env @ [(TermC.str2term "h_h::bool", TermC.str2term s')];
14.681 -=== inhibit exn 110726=============================================================*)
14.682 -
14.683 -(*--- 2.line in script ---*)
14.684 -val t = TermC.str2term "dropWhile (ident (h_h::bool)) (eqs::bool list)";
14.685 -val s = subst_atomic env t;
14.686 -UnparseC.term s;
14.687 -val t = TermC.str2term
14.688 -"dropWhile (ident (A = a * b))\
14.689 -\ [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
14.690 -(*=== inhibit exn 110726=============================================================
14.691 -val SOME (t',_) = rewrite_set_ thy false prog_expr t;
14.692 -val s' = UnparseC.term t';
14.693 -if s' = "[a / 2 = r * sin alpha, b / 2 = r * cos alpha]"
14.694 -then () else error "new behaviour with prog_expr 3.2.";
14.695 -=== inhibit exn 110726=============================================================*)
14.696 -val env = env @ [(TermC.str2term "es_s::bool list", TermC.str2term s')];
14.697 -
14.698 -(*--- 3.line in script ---*)
14.699 -val t = TermC.str2term "dropWhile (ident (f_f::real)) (Vars (h_h::bool))";
14.700 -val s = subst_atomic env t;
14.701 -UnparseC.term s;
14.702 -val t = TermC.str2term "dropWhile (ident A) (Vars (A = a * b))";
14.703 -(*=== inhibit exn 110726=============================================================
14.704 -val SOME (t',_) = rewrite_set_ thy false prog_expr t;
14.705 -val s' = UnparseC.term t';
14.706 -if s' = "[a, b]" then () else error "new behaviour with prog_expr 3.3.";
14.707 -=== inhibit exn 110726=============================================================*)
14.708 -val env = env @ [(TermC.str2term "vs_s::real list", TermC.str2term s')];
14.709 -
14.710 -(*--- 4.line in script ---*)
14.711 -val t = TermC.str2term "nth_h 1 v_s";
14.712 -val s = subst_atomic env t;
14.713 -UnparseC.term s;
14.714 -val t = TermC.str2term "nth_h 1 [a, b]";
14.715 -(*=== inhibit exn 110726=============================================================
14.716 -val SOME (t',_) = rewrite_set_ thy false prog_expr t;
14.717 -val s' = UnparseC.term t';
14.718 -if s' = "a" then () else error "new behaviour with prog_expr 3.4.";
14.719 -=== inhibit exn 110726=============================================================*)
14.720 -val env = env @ [(TermC.str2term "v_1", TermC.str2term s')];
14.721 -
14.722 -(*--- 5.line in script ---*)
14.723 -val t = TermC.str2term "nth_h 2 v_s";
14.724 -val s = subst_atomic env t;
14.725 -UnparseC.term s;
14.726 -val t = TermC.str2term "nth_h 2 [a, b]";
14.727 -(*=== inhibit exn 110726=============================================================
14.728 -val SOME (t',_) = rewrite_set_ thy false prog_expr t;
14.729 -val s' = UnparseC.term t';
14.730 -if s' = "b" then () else error "new behaviour with prog_expr 3.5.";
14.731 -=== inhibit exn 110726=============================================================*)
14.732 -val env = env @ [(TermC.str2term "v_2", TermC.str2term s')];
14.733 -
14.734 -(*--- 6.line in script ---*)
14.735 -val t = TermC.str2term "(hd o (filterVar v_1)) (es_s::bool list)";
14.736 -val s = subst_atomic env t;
14.737 -UnparseC.term s;
14.738 -val t = TermC.str2term
14.739 - "(hd o filterVar a) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
14.740 -val SOME (t',_) = rewrite_set_ thy false prog_expr t;
14.741 -val s' = UnparseC.term t';
14.742 -(*=== inhibit exn 110726=============================================================
14.743 -if s' = "a / 2 = r * sin alpha" then ()
14.744 -else error "new behaviour with prog_expr 3.6.";
14.745 -=== inhibit exn 110726=============================================================*)
14.746 -val e_1 = TermC.str2term "e_1::bool";
14.747 -val env = env @ [(e_1, TermC.str2term s')];
14.748 -
14.749 -(*--- 7.line in script ---*)
14.750 -val t = TermC.str2term "(hd o (filterVar v_2)) (es_s::bool list)";
14.751 -val s = subst_atomic env t;
14.752 -UnparseC.term s;
14.753 -val t = TermC.str2term
14.754 - "(hd o filterVar b) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
14.755 -val SOME (t',_) = rewrite_set_ thy false prog_expr t;
14.756 -val s' = UnparseC.term t';
14.757 -(*=== inhibit exn 110726=============================================================
14.758 -if s' = "b / 2 = r * cos alpha" then ()
14.759 -else error "new behaviour with prog_expr 3.7.";
14.760 -=== inhibit exn 110726=============================================================*)
14.761 -val env = env @ [(TermC.str2term "e_2::bool", TermC.str2term s')];
14.762 -
14.763 -(*--- 8.line in script ---*)
14.764 -val t = TermC.str2term "(SubProblem (Reals_s,[univar,equation],[no_met])\
14.765 - \ [BOOL e_1, REAL v_1])";
14.766 -val s = subst_atomic env t;
14.767 -UnparseC.term s;
14.768 -"SubProblem (Reals_s, [univar, equation], [no_met])\
14.769 - \ [BOOL (a / 2 = r * sin alpha), REAL a]";
14.770 -val s_1 = TermC.str2term "[a = 2*r*sin alpha]";
14.771 -val env = env @ [(TermC.str2term "s_1::bool list", s_1)];
14.772 -
14.773 -(*--- 9.line in script ---*)
14.774 -val t = TermC.str2term "(SubProblem (Reals_s,[univar,equation],[no_met])\
14.775 - \ [BOOL e_2, REAL v_2])";
14.776 -val s = subst_atomic env t;
14.777 -UnparseC.term s;
14.778 -"SubProblem (Reals_s, [univar, equation], [no_met])\
14.779 - \ [BOOL (b / 2 = r * cos alpha), REAL b]";
14.780 -val s_2 = TermC.str2term "[b = 2*r*cos alpha]";
14.781 -val env = env @ [(TermC.str2term "s_2::bool list", s_2)];
14.782 -
14.783 -(*--- 10.line in script ---*)
14.784 -val t = TermC.str2term
14.785 -"Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] (h_h::bool)";
14.786 -val s = subst_atomic env t;
14.787 -UnparseC.term s;
14.788 -"Substitute\n [(a = (rhs o hd) [a = 2 * r * sin alpha]),\
14.789 -\ (b = (rhs o hd) [b = 2 * r * cos alpha])] (A = a * b)";
14.790 -val SOME (s',_) = rewrite_set_ thy false prog_expr s;
14.791 -val s'' = UnparseC.term s';
14.792 -(*=== inhibit exn 110726=============================================================
14.793 -if s'' =
14.794 -"Substitute [a = 2 * r * sin alpha, b = 2 * r * cos alpha] (A = a * b)"
14.795 -then () else error "new behaviour with prog_expr 3.10.";
14.796 -===== inhibit exn 110722===========================================================*)
14.797 -
15.1 --- a/test/Tools/isac/MathEngine/step.sml Fri Jun 17 12:15:09 2022 +0200
15.2 +++ b/test/Tools/isac/MathEngine/step.sml Sat Jun 18 12:34:29 2022 +0200
15.3 @@ -267,8 +267,8 @@
15.4 "interval {x::real. 0 <= x & x <= pi}",
15.5 "errorBound (eps=(0::real))"];
15.6 val (dI',pI',mI') =
15.7 - ("DiffApp",["maximum_of", "function"],
15.8 - ["DiffApp", "max_by_calculus"]);
15.9 + ("Diff_App",["maximum_of", "function"],
15.10 + ["Diff_App", "max_by_calculus"]);
15.11 val c = []:cid;
15.12
15.13 val (p,_,f, nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
15.14 @@ -302,13 +302,13 @@
15.15 "(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(r_s, [[A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]"
15.16 then () else error "maximum example add_items changed";
15.17
15.18 -val ("ok", ([(Specify_Theory "DiffApp", _, _)], _, ptp))
15.19 +val ("ok", ([(Specify_Theory "Diff_App", _, _)], _, ptp))
15.20 = Step.specify_do_next ptp;
15.21
15.22 val ("ok", ([(Specify_Problem ["maximum_of", "function"], _, _)], _, ptp))
15.23 = Step.specify_do_next ptp;
15.24
15.25 -val ("ok", ([(Specify_Method ["DiffApp", "max_by_calculus"], _, _)], _, ptp))
15.26 +val ("ok", ([(Specify_Method ["Diff_App", "max_by_calculus"], _, _)], _, ptp))
15.27 = Step.specify_do_next ptp;
15.28
15.29 val ("ok", ([(Add_Given "boundVariable a", _, _)], _, ptp))
15.30 @@ -343,8 +343,8 @@
15.31 "interval {x::real. 0 <= x & x <= pi}",
15.32 "errorBound (eps=(0::real))"];
15.33 val (dI',pI',mI') =
15.34 - ("DiffApp",["maximum_of", "function"],
15.35 - ["DiffApp", "max_by_calculus"]);
15.36 + ("Diff_App",["maximum_of", "function"],
15.37 + ["Diff_App", "max_by_calculus"]);
15.38 val c = []:cid;
15.39 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
15.40
15.41 @@ -385,7 +385,7 @@
15.42 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
15.43 ------------------------------ FIXXXXME.me !!! ---*)
15.44
15.45 -(*val nxt = Specify_Theory "DiffApp" : tac*)
15.46 +(*val nxt = Specify_Theory "Diff_App" : tac*)
15.47
15.48 val itms = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt itms);
15.49
15.50 @@ -395,7 +395,7 @@
15.51
15.52 val nxt = tac2tac_ pt p nxt;
15.53 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
15.54 -(*val nxt = Specify_Method ("DiffApp", "max_by_calculus")*)
15.55 +(*val nxt = Specify_Method ("Diff_App", "max_by_calculus")*)
15.56
15.57 val nxt = tac2tac_ pt p nxt;
15.58 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
15.59 @@ -411,8 +411,8 @@
15.60
15.61 val nxt = tac2tac_ pt p nxt;
15.62 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
15.63 -(*val nxt = Apply_Method ("DiffApp", "max_by_calculus") *)
15.64 -case nxt of (Apply_Method ["DiffApp", "max_by_calculus"]) => ()
15.65 +(*val nxt = Apply_Method ("Diff_App", "max_by_calculus") *)
15.66 +case nxt of (Apply_Method ["Diff_App", "max_by_calculus"]) => ()
15.67 | _ => error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus";
15.68
15.69
15.70 @@ -430,7 +430,7 @@
15.71 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
15.72 (*val nxt = Specify_Theory ThyC.id_empty : tac*)
15.73
15.74 -val nxt = Specify_Theory "DiffApp";
15.75 +val nxt = Specify_Theory "Diff_App";
15.76 val nxt = tac2tac_ pt p nxt;
15.77 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
15.78 (*val nxt = Specify_Problem Problem.id_empty : tac*)
15.79 @@ -471,7 +471,7 @@
15.80 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
15.81 (*val nxt = Specify_Method (ThyC.id_empty, MethodC.id_empty) : tac*)
15.82
15.83 -val nxt = Specify_Method ["DiffApp", "max_by_calculus"];
15.84 +val nxt = Specify_Method ["Diff_App", "max_by_calculus"];
15.85 val nxt = tac2tac_ pt p nxt;
15.86 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
15.87 (*val nxt = Add_Given "boundVariable" : tac*)
15.88 @@ -489,15 +489,15 @@
15.89 val nxt = Add_Given "errorBound (eps=999)";
15.90 val nxt = tac2tac_ pt p nxt;
15.91 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
15.92 -(*val nxt = Apply_Method ("DiffApp", "max_by_calculus") *)
15.93 +(*val nxt = Apply_Method ("Diff_App", "max_by_calculus") *)
15.94
15.95 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
15.96 -if nxt<>(Apply_Method ("DiffApp", "max_by_calculus"))
15.97 +if nxt<>(Apply_Method ("Diff_App", "max_by_calculus"))
15.98 then error "test specify, fmz <> []: nxt <> Add_Relation.."
15.99 else ();
15.100 *)
15.101 (* 2.4.00 nach Transfer specify -> hard_gen
15.102 -val nxt = Apply_Method ("DiffApp", "max_by_calculus");
15.103 +val nxt = Apply_Method ("Diff_App", "max_by_calculus");
15.104 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; *)
15.105 (*val nxt = Empty_Tac : tac*)
15.106 ------------------------------------------------------ after specify --> Step.specify_find_next *)
16.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Fri Jun 17 12:15:09 2022 +0200
16.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Sat Jun 18 12:34:29 2022 +0200
16.3 @@ -400,15 +400,15 @@
16.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
16.5 (* val nxt = ("Add_Find",Add_Find "solutions L"); *)
16.6 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
16.7 -(* val nxt = ("Specify_Theory",Specify_Theory "DiffAppl");
16.8 +(* val nxt = ("Specify_Theory",Specify_Theory "Diff_Appl");
16.9 > get_obj g_spec pt (fst p);
16.10 val it = (ThyC.id_empty,Problem.id_empty,(ThyC.id_empty, MethodC.id_empty)) : spec*)
16.11 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
16.12 (*val nxt = ("Specify_Problem", Specify_Problem *)
16.13 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
16.14 -(*val nxt = ("Specify_Method",Specify_Method ("DiffAppl", "sqrt-equ-test"));*)
16.15 +(*val nxt = ("Specify_Method",Specify_Method ("Diff_Appl", "sqrt-equ-test"));*)
16.16 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
16.17 -(*val nxt = ("Apply_Method",Apply_Method ("DiffAppl", "sqrt-equ-test"));*)
16.18 +(*val nxt = ("Apply_Method",Apply_Method ("Diff_Appl", "sqrt-equ-test"));*)
16.19 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
16.20 val nxt = ("Free_Solve",Free_Solve);
16.21 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17.1 --- a/test/Tools/isac/OLDTESTS/script.sml Fri Jun 17 12:15:09 2022 +0200
17.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Sat Jun 18 12:34:29 2022 +0200
17.3 @@ -38,7 +38,7 @@
17.4 " scripts: Variante 'funktional' 6.5.03";
17.5 " ################################################# 6.5.03 ";
17.6
17.7 -val c = (the o (TermC.parse DiffApp.thy))
17.8 +val c = (the o (TermC.parse Diff_App.thy))
17.9 "Program Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
17.10 \ (v_::real) (itv_::real set) (err_::bool) = \
17.11 \ (let e_e = (hd o (filterVar m_)) rs_; \
17.12 @@ -58,7 +58,7 @@
17.13 "############## Make_fun_by_new_variable ########### 6.5.03";
17.14 "################################################### 6.5.03";
17.15
17.16 -val sc = (the o (TermC.parse DiffApp.thy)) (*start interpretieren*)
17.17 +val sc = (the o (TermC.parse Diff_App.thy)) (*start interpretieren*)
17.18 "Program Make_fun_by_new_variable (f_::real) (v_::real) \
17.19 \ (eqs_::bool list) = \
17.20 \(let h_ = (hd o (filterVar f_)) eqs_; \
17.21 @@ -74,7 +74,7 @@
17.22 \ [BOOL e_2, REAL v_2])\
17.23 \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)";
17.24
17.25 -val ags = map (Thm.term_of o the o (TermC.parse DiffApp.thy))
17.26 +val ags = map (Thm.term_of o the o (TermC.parse Diff_App.thy))
17.27 ["A::real", "alpha::real",
17.28 "[A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]"];
17.29 val ll = [](*:loc_*);
17.30 @@ -92,19 +92,19 @@
17.31 val SOME(l1,t1) = same_tacpbl sc ll (mI1,m1);
17.32 loc_2str l1;
17.33 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
17.34 -Syntax.string_of_term (ThyC.id_to_ctxt "DiffApp") t1;
17.35 +Syntax.string_of_term (ThyC.id_to_ctxt "Diff_App") t1;
17.36 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *)
17.37
17.38 val SOME(l2,t2) = same_tacpbl sc l1 (mI2,m2);
17.39 loc_2str l2;
17.40 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
17.41 -Syntax.string_of_term (ThyC.id_to_ctxt "DiffApp") t2;
17.42 +Syntax.string_of_term (ThyC.id_to_ctxt "Diff_App") t2;
17.43 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *)
17.44
17.45 val SOME(l3,t3) = same_tacpbl sc l2 (mI3,m3);
17.46 loc_2str l3;
17.47 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*)
17.48 -Syntax.string_of_term (ThyC.id_to_ctxt "DiffApp") t3;
17.49 +Syntax.string_of_term (ThyC.id_to_ctxt "Diff_App") t3;
17.50 (*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*)
17.51
17.52
17.53 @@ -141,7 +141,7 @@
17.54 "############## Make_fun_by_explicit ############## 6.5.03";
17.55 "############## Make_fun_by_explicit ############## 6.5.03";
17.56 "############## Make_fun_by_explicit ############## 6.5.03";
17.57 -val c = (the o (TermC.parse DiffApp.thy))
17.58 +val c = (the o (TermC.parse Diff_App.thy))
17.59 "Program Make_fun_by_explicit (f_::real) (v_::real) \
17.60 \ (eqs_::bool list) = \
17.61 \ (let h_ = (hd o (filterVar f_)) eqs_; \
18.1 --- a/test/Tools/isac/Specify/refine.thy Fri Jun 17 12:15:09 2022 +0200
18.2 +++ b/test/Tools/isac/Specify/refine.thy Sat Jun 18 12:34:29 2022 +0200
18.3 @@ -16,28 +16,28 @@
18.4 setup \<open>KEStore_Elems.add_pbts
18.5 [(Problem.prep_input @{theory} "pbl_test_refine" [] Problem.id_empty
18.6 (["refine", "test"], [], Rule_Set.empty, NONE, [])),
18.7 -(Problem.prep_input @{theory DiffApp} "pbl_pbla" [] Problem.id_empty
18.8 +(Problem.prep_input @{theory Diff_App} "pbl_pbla" [] Problem.id_empty
18.9 (["pbla", "refine", "test"],
18.10 [("#Given", ["fixedValues a_a"])], Rule_Set.empty, NONE, [])),
18.11 -(Problem.prep_input @{theory DiffApp} "pbl_pbla1" [] Problem.id_empty
18.12 +(Problem.prep_input @{theory Diff_App} "pbl_pbla1" [] Problem.id_empty
18.13 (["pbla1", "pbla", "refine", "test"],
18.14 [("#Given", ["fixedValues a_a", "maximum a_1"])], Rule_Set.empty, NONE, [])),
18.15 -(Problem.prep_input @{theory DiffApp} "pbl_pbla2" [] Problem.id_empty
18.16 +(Problem.prep_input @{theory Diff_App} "pbl_pbla2" [] Problem.id_empty
18.17 (["pbla2", "pbla", "refine", "test"],
18.18 [("#Given", ["fixedValues a_a", "valuesFor a_2"])], Rule_Set.empty, NONE, [])),
18.19 -(Problem.prep_input @{theory DiffApp} "pbl_pbla2x" [] Problem.id_empty
18.20 +(Problem.prep_input @{theory Diff_App} "pbl_pbla2x" [] Problem.id_empty
18.21 (["pbla2x", "pbla2", "pbla", "refine", "test"],
18.22 [("#Given", ["fixedValues a_a", "valuesFor a_2", "functionOf a2_x"])],
18.23 Rule_Set.empty, NONE, [])),
18.24 -(Problem.prep_input @{theory DiffApp} "pbl_pbla2y" [] Problem.id_empty
18.25 +(Problem.prep_input @{theory Diff_App} "pbl_pbla2y" [] Problem.id_empty
18.26 (["pbla2y", "pbla2", "pbla", "refine", "test"],
18.27 [("#Given" ,["fixedValues a_a", "valuesFor a_2", "boundVariable a2_y"])],
18.28 Rule_Set.empty, NONE, [])),
18.29 -(Problem.prep_input @{theory DiffApp} "pbl_pbla2z" [] Problem.id_empty
18.30 +(Problem.prep_input @{theory Diff_App} "pbl_pbla2z" [] Problem.id_empty
18.31 (["pbla2z", "pbla2", "pbla", "refine", "test"],
18.32 [("#Given" ,["fixedValues a_a", "valuesFor a_2", "interval a2_z"])],
18.33 Rule_Set.empty, NONE, [])),
18.34 -(Problem.prep_input @{theory DiffApp} "pbl_pbla3" [] Problem.id_empty
18.35 +(Problem.prep_input @{theory Diff_App} "pbl_pbla3" [] Problem.id_empty
18.36 (["pbla3", "pbla", "refine", "test"],
18.37 [("#Given" ,["fixedValues a_a", "relations a_3"])],
18.38 Rule_Set.empty, NONE, []))]
19.1 --- a/test/Tools/isac/Specify/specify.sml Fri Jun 17 12:15:09 2022 +0200
19.2 +++ b/test/Tools/isac/Specify/specify.sml Sat Jun 18 12:34:29 2022 +0200
19.3 @@ -31,7 +31,7 @@
19.4 "interval {x::real. 0 <= x & x <= 2*r}",
19.5 "interval {x::real. 0 <= x & x <= pi}",
19.6 "errorBound (eps=(0::real))"],
19.7 - ("DiffApp",["maximum_of", "function"],["DiffApp", "max_by_calculus"])
19.8 + ("Diff_App",["maximum_of", "function"],["Diff_App", "max_by_calculus"])
19.9 )];
19.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.12 @@ -88,7 +88,7 @@
19.13 "interval {x::real. 0 <= x & x <= 2*r}",
19.14 "interval {x::real. 0 <= x & x <= pi}",
19.15 "errorBound (eps=(0::real))"],
19.16 - ("DiffApp",["maximum_of", "function"],["DiffApp", "max_by_calculus"])
19.17 + ("Diff_App",["maximum_of", "function"],["Diff_App", "max_by_calculus"])
19.18 )];
19.19 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.20 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.21 @@ -97,7 +97,7 @@
19.22 val (p,_,f,nxt,_,pt) = (me nxt p c pt) (*handle e => OldGoals.print_exn e;*)
19.23 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.24 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.25 - (*nxt = Specify_Theory "DiffApp"*)
19.26 + (*nxt = Specify_Theory "Diff_App"*)
19.27 val (oris, _, _) = get_obj g_origin pt (fst p);
19.28 writeln (O_Model.to_string oris);
19.29 (*[
19.30 @@ -122,7 +122,7 @@
19.31 2 = r \<up> 2] ,(rs_, [[A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]*)
19.32 val mits = get_obj g_met pt (fst p);
19.33 val mits = I_Model.complete oris pits []
19.34 - ((#ppc o MethodC.from_store) ["DiffApp", "max_by_calculus"]);
19.35 + ((#ppc o MethodC.from_store) ["Diff_App", "max_by_calculus"]);
19.36 writeln (I_Model.to_string ctxt mits);
19.37 (*[
19.38 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
20.1 --- a/test/Tools/isac/Test_Isac.thy Fri Jun 17 12:15:09 2022 +0200
20.2 +++ b/test/Tools/isac/Test_Isac.thy Sat Jun 18 12:34:29 2022 +0200
20.3 @@ -303,7 +303,7 @@
20.4 ML_file "Knowledge/test.sml"
20.5 ML_file "Knowledge/polyminus.sml"
20.6 ML_file "Knowledge/vect.sml"
20.7 - ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
20.8 + ML_file "Knowledge/diff-app.sml" (* postponed to dev. specification | TP-prog. *)
20.9 ML_file "Knowledge/biegelinie-1.sml"
20.10 ML_file "Knowledge/biegelinie-2.sml" (*Test_Isac_Short*)
20.11 ML_file "Knowledge/biegelinie-3.sml" (*Test_Isac_Short*)
21.1 --- a/test/Tools/isac/Test_Isac_Short.thy Fri Jun 17 12:15:09 2022 +0200
21.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Sat Jun 18 12:34:29 2022 +0200
21.3 @@ -306,7 +306,7 @@
21.4 ML_file "Knowledge/test.sml"
21.5 ML_file "Knowledge/polyminus.sml"
21.6 ML_file "Knowledge/vect.sml"
21.7 - ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
21.8 + ML_file "Knowledge/diff-app.sml" (* postponed to dev. specification | TP-prog. *)
21.9 ML_file "Knowledge/biegelinie-1.sml"
21.10 (*ML_file "Knowledge/biegelinie-2.sml" Test_Isac_Short*)
21.11 (*ML_file "Knowledge/biegelinie-3.sml" Test_Isac_Short*)