1.1 --- a/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml Sun Apr 25 12:03:49 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml Sun Apr 25 12:49:37 2021 +0200
1.3 @@ -37,7 +37,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"]};
1.7 -(* ^^^ is exponenation *)
1.8 +(* \<up> is exponenation *)
1.9
1.10 (* the functions Ex_frees, Rhs provide for the instantiation below *)
1.11
1.12 @@ -46,11 +46,11 @@
1.13 where_= ["is_equality (R = #7)",
1.14 "Not (R <= #0)"],
1.15 find =["maximum A", "values_for [a,b]"],
1.16 - with_ =["EX A. A = a*b & (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2 \
1.17 - \ (ALL A'. A' = a*b & (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2 \
1.18 + with_ =["EX A. A = a*b & (a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2 \
1.19 + \ (ALL A'. A' = a*b & (a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2 \
1.20 \ --> A' <= A)))"],
1.21 relate=["max_relation (A = a*b)",
1.22 - "additionalRels [(a//#2)^^^#2 +(b//#2)^^^#2 =R^^^#2]"]};
1.23 + "additionalRels [(a//#2) \<up> #2 +(b//#2) \<up> #2 =R \<up> #2]"]};
1.24 (* R,a,b are bound by given, find *)
1.25
1.26 (* (2) instantiation of maximum *)
1.27 @@ -79,9 +79,9 @@
1.28
1.29 (* (1) instantiation for make-explicit-and-substitute *)
1.30 {given = ["equality A = a * b", "bound_variable a",
1.31 - "equalities [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"],
1.32 + "equalities [(a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2]"],
1.33 where_= [],
1.34 - find = ["function_term A_"(*=(a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))*)],
1.35 + find = ["function_term A_"(*=(a * #2 * sqrt(R \<up> #2 - (a//#2) \<up> #2))*)],
1.36 with_ = [],
1.37 relate= []};
1.38
1.39 @@ -108,14 +108,14 @@
1.40 (* ':' is 'element', '::' is a type constraint *)
1.41
1.42 (* (1) variant of instantiation *)
1.43 -{given = ["function_term (a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))",
1.44 +{given = ["function_term (a * #2 * sqrt(R \<up> #2 - (a//#2) \<up> #2))",
1.45 "bound_variable a",
1.46 "domain {x::real. #0 <= x & x <= #2*R}"],
1.47 where_= [],
1.48 find = ["maximums AM"],
1.49 with_ = ["ALL am. am : AM --> \
1.50 \ (ALL x::real. #0 <= x & x <= #2*R \
1.51 - \ --> (%a. (a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))) x <= am)"],
1.52 + \ --> (%a. (a * #2 * sqrt(R \<up> #2 - (a//#2) \<up> #2))) x <= am)"],
1.53 relate= []};
1.54
1.55 (* (2) variant of instantiation *)
1.56 @@ -163,7 +163,7 @@
1.57
1.58 (* (1) variant of instantiation *)
1.59 {given = ["max_relation (A = a*b)",
1.60 - "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]"],
1.61 + "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2]"],
1.62 where_= [],
1.63 find = ["values_for [a,b]"],
1.64 with_ = [],
1.65 @@ -225,7 +225,7 @@
1.66 parse thy "if a=b then a else b";
1.67 parse thy "maxmin = is_max";
1.68 parse thy "maxmin =!= is_max";
1.69 - ^^^--- geht nicht wegen fun-types *)
1.70 + \<up> --- geht nicht wegen fun-types *)
1.71
1.72 "pbltyp --- maximum ---";
1.73 val pbltyp = {given=["fixed_values (cs::bool list)"],
1.74 @@ -244,18 +244,18 @@
1.75 "domain {x::real. #0 <= x & x <= #2*R}",
1.76 "domain {x::real. #0 <= x & x <= pi}",
1.77 "maximum A",
1.78 - "max_relation A=#2*a*b - a^^^#2",
1.79 - "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
1.80 - "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
1.81 + "max_relation A=#2*a*b - a \<up> #2",
1.82 + "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2]",
1.83 + "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2]",
1.84 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"];
1.85 val chkorg = map (the o (parse thy)) org;
1.86 val pbl = {given=["fixed_values [R=(R::real)]"],where_=[],
1.87 find=["maximum A", "values_for [a,b]"],
1.88 - with_=["EX alpha. A=#2*a*b - a^^^#2 & \
1.89 + with_=["EX alpha. A=#2*a*b - a \<up> #2 & \
1.90 \ a=#2*R*sin alpha & b=#2*R*cos alpha & \
1.91 - \ (ALL A'. A'=#2*a*b - a^^^#2 & a=#2*R*sin alpha & b=#2*R*cos alpha \
1.92 + \ (ALL A'. A'=#2*a*b - a \<up> #2 & a=#2*R*sin alpha & b=#2*R*cos alpha \
1.93 \ --> A' <= A)"],
1.94 - relate=["max_relation (A=#2*a*b - a^^^#2)",
1.95 + relate=["max_relation (A=#2*a*b - a \<up> #2)",
1.96 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
1.97 }: string ppc;
1.98 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
1.99 @@ -287,7 +287,7 @@
1.100 relate=[(*???*)]}: string ppc;
1.101 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
1.102 "coil";
1.103 -val pbl = {given=["equality (A=#2*a*b - a^^^#2)", "bound_variable alpha",
1.104 +val pbl = {given=["equality (A=#2*a*b - a \<up> #2)", "bound_variable alpha",
1.105 "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
1.106 where_=[],
1.107 find=["function_term t"],
1.108 @@ -320,7 +320,7 @@
1.109 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
1.110 "coil";
1.111 val pbl = {given=["function_term #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \
1.112 - \ (#2*R*sin alpha)^^^#2", "bound_variable alpha",
1.113 + \ (#2*R*sin alpha) \<up> #2", "bound_variable alpha",
1.114 "domain {x::real. #0 <= x & x <= pi}"],where_=[],
1.115 find=["maximums [#1234]"],with_=[],relate=[]}: string ppc;
1.116 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
1.117 @@ -354,7 +354,7 @@
1.118 "p.117";
1.119 val org = {given=["[r=#5]"],where_=[],
1.120 find=["[x,(y::real)]"],with_=[],
1.121 - relate=["[is_max #0=pi*x^^^#2 + pi*x*(r::real)]"]}: string ppc;
1.122 + relate=["[is_max #0=pi*x \<up> #2 + pi*x*(r::real)]"]}: string ppc;
1.123 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
1.124 "#241";
1.125 val org = {given=["[s=(#10::real)]"],where_=[],