1.1 --- a/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml Sat May 16 16:23:24 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml Sat May 16 16:54:39 2020 +0200
1.3 @@ -236,7 +236,7 @@
1.4 \ (ALL m'. (subst (m,m') (foldl (op &) True (r#rs)) \
1.5 \ --> m' <= m)))"],
1.6 relate=["max_relation r","additionalRels rs"]}:string ppc;
1.7 -val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
1.8 +val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
1.9 "coil";
1.10 val org = ["fixed_values [R=(R::real)]",
1.11 "bound_variable a", "bound_variable b", "bound_variable alpha",
1.12 @@ -258,7 +258,7 @@
1.13 relate=["max_relation (A=#2*a*b - a^^^#2)",
1.14 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
1.15 }: string ppc;
1.16 -val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
1.17 +val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
1.18
1.19 "met --- maximum_by_differentiation ---";
1.20 val met = {given=["fixed_values (cs::bool list)","bound_variable v",
1.21 @@ -274,7 +274,7 @@
1.22 \( ALL x. lower_bound <= x & x <= upper_bound \
1.23 \ --> (%v. t) x <= m)"],
1.24 relate=["rs::bool list"]}: string ppc;
1.25 -val chkpbl = ((map (the o (parse thy))) o ppc2list) met;
1.26 +val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) met;
1.27
1.28
1.29 "pbltyp --- make_fun ---";
1.30 @@ -285,27 +285,27 @@
1.31 where_=[],
1.32 find=["function_term t"],with_=[(*???*)],
1.33 relate=[(*???*)]}: string ppc;
1.34 -val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
1.35 +val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
1.36 "coil";
1.37 val pbl = {given=["equality (A=#2*a*b - a^^^#2)","bound_variable alpha",
1.38 "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
1.39 where_=[],
1.40 find=["function_term t"],
1.41 with_=[],relate=[]}: string ppc;
1.42 -val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
1.43 +val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
1.44
1.45 "met --- make_explicit_and_substitute ---";
1.46 val met = {given=["equality e","bound_variable v", "equalities es"],
1.47 where_=[],
1.48 find=["function_term t"],with_=[(*???*)],
1.49 relate=[(*???*)]}: string ppc;
1.50 -val chkmet = ((map (the o (parse thy))) o ppc2list) met;
1.51 +val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met;
1.52 "met --- introduce_a_new_variable ---";
1.53 val met = {given=["equality e","bound_variable v", "substitutions es"],
1.54 where_=[],
1.55 find=["function_term t"],with_=[(*???*)],
1.56 relate=[(*???*)]}: string ppc;
1.57 -val chkmet = ((map (the o (parse thy))) o ppc2list) met;
1.58 +val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met;
1.59
1.60
1.61 "pbltyp --- max_of_fun_on_interval ---";
1.62 @@ -317,13 +317,13 @@
1.63 \ (ALL x::real. lower_bound <= x & x <= upper_bound \
1.64 \ --> (%v. t) x <= m)"],
1.65 relate=[]}: string ppc;
1.66 -val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
1.67 +val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
1.68 "coil";
1.69 val pbl = {given=["function_term #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \
1.70 \ (#2*R*sin alpha)^^^#2","bound_variable alpha",
1.71 "domain {x::real. #0 <= x & x <= pi}"],where_=[],
1.72 find=["maximums [#1234]"],with_=[],relate=[]}: string ppc;
1.73 -val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
1.74 +val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
1.75
1.76
1.77 (* pbltyp --- max_of_fun --- *)
1.78 @@ -345,22 +345,22 @@
1.79 val org = {given=["[u=(#12::real)]"],where_=[],
1.80 find=["[a,(b::real)]"],with_=[],
1.81 relate=["[is_max A=a*(b::real), #2*a+#2*b=(u::real)]"]}: string ppc;
1.82 -val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.83 +val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
1.84 "p.116";
1.85 val org = {given=["[c=#10, h=(#4::real)]"],where_=[],
1.86 find=["[x,(y::real)]"],with_=[],
1.87 relate=["[A=x*(y::real), c//h=x//(h-(y::real))]"]}: string ppc;
1.88 -val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.89 +val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
1.90 "p.117";
1.91 val org = {given=["[r=#5]"],where_=[],
1.92 find=["[x,(y::real)]"],with_=[],
1.93 relate=["[is_max #0=pi*x^^^#2 + pi*x*(r::real)]"]}: string ppc;
1.94 -val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.95 +val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
1.96 "#241";
1.97 val org = {given=["[s=(#10::real)]"],where_=[],
1.98 find=["[p::real]"],with_=[],
1.99 relate=["[is_max p=n*m, s=n+(m::real)]"]}: string ppc;
1.100 -val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.101 +val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
1.102
1.103 (*
1.104 {given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;