1.1 --- a/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml Mon Oct 31 18:28:36 2022 +0100
1.2 +++ b/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml Mon Nov 07 17:37:20 2022 +0100
1.3 @@ -104,7 +104,7 @@
1.4 with_ = ["ALL m. m : ms --> \
1.5 \ (ALL x::real. lower_bound <= x & x <= upper_bound \
1.6 \ --> (%v. t) x <= m)"],
1.7 - relate= []}: string ppc;
1.8 + relate= []}: string model;
1.9 (* ':' is 'element', '::' is a type constraint *)
1.10
1.11 (* (1) variant of instantiation *)
1.12 @@ -235,7 +235,7 @@
1.13 with_=["Ex_frees ((foldl (op &) True (r#rs)) & \
1.14 \ (ALL m'. (subst (m,m') (foldl (op &) True (r#rs)) \
1.15 \ --> m' <= m)))"],
1.16 - relate=["max_relation r", "additionalRels rs"]}:string ppc;
1.17 + relate=["max_relation r", "additionalRels rs"]}:string model;
1.18 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
1.19 "coil";
1.20 val org = ["fixed_values [R=(R::real)]",
1.21 @@ -257,7 +257,7 @@
1.22 \ --> A' <= A)"],
1.23 relate=["max_relation (A=#2*a*b - a \<up> #2)",
1.24 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
1.25 - }: string ppc;
1.26 + }: string model;
1.27 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
1.28
1.29 "met --- maximum_by_differentiation ---";
1.30 @@ -273,7 +273,7 @@
1.31 \m = (%v. t) mx & \
1.32 \( ALL x. lower_bound <= x & x <= upper_bound \
1.33 \ --> (%v. t) x <= m)"],
1.34 - relate=["rs::bool list"]}: string ppc;
1.35 + relate=["rs::bool list"]}: string model;
1.36 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) met;
1.37
1.38
1.39 @@ -284,27 +284,27 @@
1.40 val pbltyp = {given=["equality e", "bound_variable v", "equalities es"],
1.41 where_=[],
1.42 find=["function_term t"],with_=[(*???*)],
1.43 - relate=[(*???*)]}: string ppc;
1.44 + relate=[(*???*)]}: string model;
1.45 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
1.46 "coil";
1.47 val pbl = {given=["equality (A=#2*a*b - a \<up> #2)", "bound_variable alpha",
1.48 "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
1.49 where_=[],
1.50 find=["function_term t"],
1.51 - with_=[],relate=[]}: string ppc;
1.52 + with_=[],relate=[]}: string model;
1.53 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
1.54
1.55 "met --- make_explicit_and_substitute ---";
1.56 val met = {given=["equality e", "bound_variable v", "equalities es"],
1.57 where_=[],
1.58 find=["function_term t"],with_=[(*???*)],
1.59 - relate=[(*???*)]}: string ppc;
1.60 + relate=[(*???*)]}: string model;
1.61 val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met;
1.62 "met --- introduce_a_new_variable ---";
1.63 val met = {given=["equality e", "bound_variable v", "substitutions es"],
1.64 where_=[],
1.65 find=["function_term t"],with_=[(*???*)],
1.66 - relate=[(*???*)]}: string ppc;
1.67 + relate=[(*???*)]}: string model;
1.68 val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met;
1.69
1.70
1.71 @@ -316,19 +316,19 @@
1.72 with_=["ALL m. m : ms --> \
1.73 \ (ALL x::real. lower_bound <= x & x <= upper_bound \
1.74 \ --> (%v. t) x <= m)"],
1.75 - relate=[]}: string ppc;
1.76 + relate=[]}: string model;
1.77 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
1.78 "coil";
1.79 val pbl = {given=["function_term #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \
1.80 \ (#2*R*sin alpha) \<up> #2", "bound_variable alpha",
1.81 "domain {x::real. #0 <= x & x <= pi}"],where_=[],
1.82 - find=["maximums [#1234]"],with_=[],relate=[]}: string ppc;
1.83 + find=["maximums [#1234]"],with_=[],relate=[]}: string model;
1.84 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
1.85
1.86
1.87 (* pbltyp --- max_of_fun --- *)
1.88 (*
1.89 -{given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;
1.90 +{given=[],where_=[],find=[],with_=[],relate=[]}: string model;
1.91 val (SOME ct) = parse thy ;
1.92 atomty thy (Thm.term_of ct);
1.93 *)
1.94 @@ -344,26 +344,26 @@
1.95 "p.114";
1.96 val org = {given=["[u=(#12::real)]"],where_=[],
1.97 find=["[a,(b::real)]"],with_=[],
1.98 - relate=["[is_max A=a*(b::real), #2*a+#2*b=(u::real)]"]}: string ppc;
1.99 + relate=["[is_max A=a*(b::real), #2*a+#2*b=(u::real)]"]}: string model;
1.100 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
1.101 "p.116";
1.102 val org = {given=["[c=#10, h=(#4::real)]"],where_=[],
1.103 find=["[x,(y::real)]"],with_=[],
1.104 - relate=["[A=x*(y::real), c//h=x//(h-(y::real))]"]}: string ppc;
1.105 + relate=["[A=x*(y::real), c//h=x//(h-(y::real))]"]}: string model;
1.106 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
1.107 "p.117";
1.108 val org = {given=["[r=#5]"],where_=[],
1.109 find=["[x,(y::real)]"],with_=[],
1.110 - relate=["[is_max #0=pi*x \<up> #2 + pi*x*(r::real)]"]}: string ppc;
1.111 + relate=["[is_max #0=pi*x \<up> #2 + pi*x*(r::real)]"]}: string model;
1.112 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
1.113 "#241";
1.114 val org = {given=["[s=(#10::real)]"],where_=[],
1.115 find=["[p::real]"],with_=[],
1.116 - relate=["[is_max p=n*m, s=n+(m::real)]"]}: string ppc;
1.117 + relate=["[is_max p=n*m, s=n+(m::real)]"]}: string model;
1.118 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
1.119
1.120 (*
1.121 -{given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;
1.122 +{given=[],where_=[],find=[],with_=[],relate=[]}: string model;
1.123 val (SOME ct) = parse thy ;
1.124 atomty thy (Thm.term_of ct);
1.125 *)