1.1 --- a/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml Fri Feb 16 14:39:29 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml Thu Feb 22 17:55:29 2018 +0100
1.3 @@ -36,7 +36,7 @@
1.4 with_=["Ex_frees ((foldl (op &) True (r#RS)) & \
1.5 \ (ALL m'. (subst (m,m') (foldl (op &) True (r#RS)) \
1.6 \ --> m' <= m)))"],
1.7 - relate=["max_relation r","additional_relations RS"]};
1.8 + relate=["max_relation r","additionalRels RS"]};
1.9 (* ^^^ is exponenation *)
1.10
1.11 (* the functions Ex_frees, Rhs provide for the instantiation below *)
1.12 @@ -50,7 +50,7 @@
1.13 \ (ALL A'. A' = a*b & (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2 \
1.14 \ --> A' <= A)))"],
1.15 relate=["max_relation (A = a*b)",
1.16 - "additional_relations [(a//#2)^^^#2 +(b//#2)^^^#2 =R^^^#2]"]};
1.17 + "additionalRels [(a//#2)^^^#2 +(b//#2)^^^#2 =R^^^#2]"]};
1.18 (* R,a,b are bound by given, find *)
1.19
1.20 (* (2) instantiation of maximum *)
1.21 @@ -63,7 +63,7 @@
1.22 \ (ALL A'. A' = a*b & a = #2*R*sin alpha & b =#2*R*cos alpha \
1.23 \ --> A' <= A)))"],
1.24 relate=["max_relation (A = a*b)",
1.25 - "additional_relations [a=#2*R*sin alpha, b=#2*R*cos alpha]"]};
1.26 + "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]};
1.27 (* R,A are bound by given, find *)
1.28
1.29
1.30 @@ -155,7 +155,7 @@
1.31 (* find-values *)
1.32 (* ----------- *)
1.33 (* problem-type *)
1.34 -{given = ["max_relation r","additional_relations RS"],
1.35 +{given = ["max_relation r","additionalRels RS"],
1.36 where_= [],
1.37 find = ["values_for VS"],
1.38 with_ = [(*???*)],
1.39 @@ -163,7 +163,7 @@
1.40
1.41 (* (1) variant of instantiation *)
1.42 {given = ["max_relation (A = a*b)",
1.43 - "additional_relations [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]"],
1.44 + "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]"],
1.45 where_= [],
1.46 find = ["values_for [a,b]"],
1.47 with_ = [],
1.48 @@ -173,7 +173,7 @@
1.49 {given = ["max_relation (A = a*b)",],
1.50 where_= [],
1.51 find = ["values_for [A]",
1.52 - "additional_relations [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
1.53 + "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
1.54 with_ = [],
1.55 relate= []};
1.56
1.57 @@ -185,7 +185,7 @@
1.58 -------------------
1.59 maximum.#relate "max_relation r" -> "equality (lhs = rhs)"
1.60 formalization "bound_variable v" -> "bound_variable v"
1.61 -maximum.#relate "additional_relations RS"-> "equalities es"
1.62 +maximum.#relate "additionalRels RS"-> "equalities es"
1.63
1.64
1.65 maximum + make-fun -> #given.max-of-fun-on-interval
1.66 @@ -213,7 +213,7 @@
1.67 maximum + make-fun + max-of-fun-on-interval -> #given.find-values
1.68 ----------------------------------------------------------
1.69 maximum.#relate "max_relation r" -> "max_relation r"
1.70 -maximum.#relate "additional_relations RS"-> "additional_relations RS"
1.71 +maximum.#relate "additionalRels RS"-> "additionalRels RS"
1.72 *)
1.73
1.74
1.75 @@ -235,7 +235,7 @@
1.76 with_=["Ex_frees ((foldl (op &) True (r#rs)) & \
1.77 \ (ALL m'. (subst (m,m') (foldl (op &) True (r#rs)) \
1.78 \ --> m' <= m)))"],
1.79 - relate=["max_relation r","additional_relations rs"]}:string ppc;
1.80 + relate=["max_relation r","additionalRels rs"]}:string ppc;
1.81 val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
1.82 "coil";
1.83 val org = ["fixed_values [R=(R::real)]",
1.84 @@ -245,9 +245,9 @@
1.85 "domain {x::real. #0 <= x & x <= pi}",
1.86 "maximum A",
1.87 "max_relation A=#2*a*b - a^^^#2",
1.88 - "additional_relations [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
1.89 - "additional_relations [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
1.90 - "additional_relations [a=#2*R*sin alpha, b=#2*R*cos alpha]"];
1.91 + "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
1.92 + "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
1.93 + "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"];
1.94 val chkorg = map (the o (parse thy)) org;
1.95 val pbl = {given=["fixed_values [R=(R::real)]"],where_=[],
1.96 find=["maximum A","values_for [a,b]"],
1.97 @@ -256,7 +256,7 @@
1.98 \ (ALL A'. A'=#2*a*b - a^^^#2 & a=#2*R*sin alpha & b=#2*R*cos alpha \
1.99 \ --> A' <= A)"],
1.100 relate=["max_relation (A=#2*a*b - a^^^#2)",
1.101 - "additional_relations [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
1.102 + "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
1.103 }: string ppc;
1.104 val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
1.105