1.1 --- a/TODO.md Sun Apr 25 12:03:49 2021 +0200
1.2 +++ b/TODO.md Sun Apr 25 12:49:37 2021 +0200
1.3 @@ -39,10 +39,9 @@
1.4 * WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation
1.5 - clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
1.6
1.7 -* WN: investigate errors further which popped up in rewriting when replacing ^^^ by \<up> in ac7426ab0491.
1.8 - The errors occur with examples in test/../poly.sml, which do not work properly in isabisac20 either.
1.9 -
1.10 -* WN: cleanup remaining ^^^ in comments (but sometimes it is just ASCII art);
1.11 +* WN: Part.DONE cleanup remaining ^^^ in comments (but sometimes it is just ASCII art);
1.12 + Left ^^^ in doc-isac (old master-theses, etc: "x^^^#2 + #8" ... # are left, too)
1.13 + Left "ASCII art" in case of indicating comments pointing at facts ABOVE.
1.14
1.15 * WN: simplify const names like "is'_expanded": no need to imitate the escape of mixfix syntax;
1.16
2.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Sun Apr 25 12:03:49 2021 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Sun Apr 25 12:49:37 2021 +0200
2.3 @@ -74,8 +74,7 @@
2.4 | NONE => sysERROR2xml cI "error in kernel 1";
2.5 fun IteratorTEST cI = add_user cI;
2.6
2.7 -(*.create a calc-tree; for calls from java: thus ^^^ decoded to ^;
2.8 - compare "fun CalcTreeTEST" which does NOT decode.*)
2.9 +(* create a calc-tree; compare "fun CalcTreeTEST" *)
2.10 fun CalcTree [(fmz, sp)] (*for several variants lateron*) =
2.11 (case \<^try>\<open>
2.12 let
3.1 --- a/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml Sun Apr 25 12:03:49 2021 +0200
3.2 +++ b/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml Sun Apr 25 12:49:37 2021 +0200
3.3 @@ -37,7 +37,7 @@
3.4 \ (ALL m'. (subst (m,m') (foldl (op &) True (r#RS)) \
3.5 \ --> m' <= m)))"],
3.6 relate=["max_relation r", "additionalRels RS"]};
3.7 -(* ^^^ is exponenation *)
3.8 +(* \<up> is exponenation *)
3.9
3.10 (* the functions Ex_frees, Rhs provide for the instantiation below *)
3.11
3.12 @@ -46,11 +46,11 @@
3.13 where_= ["is_equality (R = #7)",
3.14 "Not (R <= #0)"],
3.15 find =["maximum A", "values_for [a,b]"],
3.16 - with_ =["EX A. A = a*b & (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2 \
3.17 - \ (ALL A'. A' = a*b & (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2 \
3.18 + with_ =["EX A. A = a*b & (a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2 \
3.19 + \ (ALL A'. A' = a*b & (a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2 \
3.20 \ --> A' <= A)))"],
3.21 relate=["max_relation (A = a*b)",
3.22 - "additionalRels [(a//#2)^^^#2 +(b//#2)^^^#2 =R^^^#2]"]};
3.23 + "additionalRels [(a//#2) \<up> #2 +(b//#2) \<up> #2 =R \<up> #2]"]};
3.24 (* R,a,b are bound by given, find *)
3.25
3.26 (* (2) instantiation of maximum *)
3.27 @@ -79,9 +79,9 @@
3.28
3.29 (* (1) instantiation for make-explicit-and-substitute *)
3.30 {given = ["equality A = a * b", "bound_variable a",
3.31 - "equalities [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"],
3.32 + "equalities [(a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2]"],
3.33 where_= [],
3.34 - find = ["function_term A_"(*=(a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))*)],
3.35 + find = ["function_term A_"(*=(a * #2 * sqrt(R \<up> #2 - (a//#2) \<up> #2))*)],
3.36 with_ = [],
3.37 relate= []};
3.38
3.39 @@ -108,14 +108,14 @@
3.40 (* ':' is 'element', '::' is a type constraint *)
3.41
3.42 (* (1) variant of instantiation *)
3.43 -{given = ["function_term (a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))",
3.44 +{given = ["function_term (a * #2 * sqrt(R \<up> #2 - (a//#2) \<up> #2))",
3.45 "bound_variable a",
3.46 "domain {x::real. #0 <= x & x <= #2*R}"],
3.47 where_= [],
3.48 find = ["maximums AM"],
3.49 with_ = ["ALL am. am : AM --> \
3.50 \ (ALL x::real. #0 <= x & x <= #2*R \
3.51 - \ --> (%a. (a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))) x <= am)"],
3.52 + \ --> (%a. (a * #2 * sqrt(R \<up> #2 - (a//#2) \<up> #2))) x <= am)"],
3.53 relate= []};
3.54
3.55 (* (2) variant of instantiation *)
3.56 @@ -163,7 +163,7 @@
3.57
3.58 (* (1) variant of instantiation *)
3.59 {given = ["max_relation (A = a*b)",
3.60 - "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]"],
3.61 + "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2]"],
3.62 where_= [],
3.63 find = ["values_for [a,b]"],
3.64 with_ = [],
3.65 @@ -225,7 +225,7 @@
3.66 parse thy "if a=b then a else b";
3.67 parse thy "maxmin = is_max";
3.68 parse thy "maxmin =!= is_max";
3.69 - ^^^--- geht nicht wegen fun-types *)
3.70 + \<up> --- geht nicht wegen fun-types *)
3.71
3.72 "pbltyp --- maximum ---";
3.73 val pbltyp = {given=["fixed_values (cs::bool list)"],
3.74 @@ -244,18 +244,18 @@
3.75 "domain {x::real. #0 <= x & x <= #2*R}",
3.76 "domain {x::real. #0 <= x & x <= pi}",
3.77 "maximum A",
3.78 - "max_relation A=#2*a*b - a^^^#2",
3.79 - "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
3.80 - "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
3.81 + "max_relation A=#2*a*b - a \<up> #2",
3.82 + "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2]",
3.83 + "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2]",
3.84 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"];
3.85 val chkorg = map (the o (parse thy)) org;
3.86 val pbl = {given=["fixed_values [R=(R::real)]"],where_=[],
3.87 find=["maximum A", "values_for [a,b]"],
3.88 - with_=["EX alpha. A=#2*a*b - a^^^#2 & \
3.89 + with_=["EX alpha. A=#2*a*b - a \<up> #2 & \
3.90 \ a=#2*R*sin alpha & b=#2*R*cos alpha & \
3.91 - \ (ALL A'. A'=#2*a*b - a^^^#2 & a=#2*R*sin alpha & b=#2*R*cos alpha \
3.92 + \ (ALL A'. A'=#2*a*b - a \<up> #2 & a=#2*R*sin alpha & b=#2*R*cos alpha \
3.93 \ --> A' <= A)"],
3.94 - relate=["max_relation (A=#2*a*b - a^^^#2)",
3.95 + relate=["max_relation (A=#2*a*b - a \<up> #2)",
3.96 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
3.97 }: string ppc;
3.98 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
3.99 @@ -287,7 +287,7 @@
3.100 relate=[(*???*)]}: string ppc;
3.101 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
3.102 "coil";
3.103 -val pbl = {given=["equality (A=#2*a*b - a^^^#2)", "bound_variable alpha",
3.104 +val pbl = {given=["equality (A=#2*a*b - a \<up> #2)", "bound_variable alpha",
3.105 "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
3.106 where_=[],
3.107 find=["function_term t"],
3.108 @@ -320,7 +320,7 @@
3.109 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
3.110 "coil";
3.111 val pbl = {given=["function_term #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \
3.112 - \ (#2*R*sin alpha)^^^#2", "bound_variable alpha",
3.113 + \ (#2*R*sin alpha) \<up> #2", "bound_variable alpha",
3.114 "domain {x::real. #0 <= x & x <= pi}"],where_=[],
3.115 find=["maximums [#1234]"],with_=[],relate=[]}: string ppc;
3.116 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
3.117 @@ -354,7 +354,7 @@
3.118 "p.117";
3.119 val org = {given=["[r=#5]"],where_=[],
3.120 find=["[x,(y::real)]"],with_=[],
3.121 - relate=["[is_max #0=pi*x^^^#2 + pi*x*(r::real)]"]}: string ppc;
3.122 + relate=["[is_max #0=pi*x \<up> #2 + pi*x*(r::real)]"]}: string ppc;
3.123 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
3.124 "#241";
3.125 val org = {given=["[s=(#10::real)]"],where_=[],
4.1 --- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Sun Apr 25 12:03:49 2021 +0200
4.2 +++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Sun Apr 25 12:49:37 2021 +0200
4.3 @@ -29,20 +29,20 @@
4.4 "domain {x::real. #0 <= x & x <= pi}",
4.5 "errorBound (eps = #1//#1000)",
4.6 "maximum A",
4.7 - (*"max_relation A=#2*a*b - a^^^#2",*)
4.8 - "relations [A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
4.9 - "relations [A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
4.10 - "relations [A=#2*a*b - a^^^#2, a=#2*R*sin alpha, b=#2*R*cos alpha]"];
4.11 + (*"max_relation A=#2*a*b - a \<up> #2",*)
4.12 + "relations [A=#2*a*b - a \<up> #2, (a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2]",
4.13 + "relations [A=#2*a*b - a \<up> #2, (a//#2) \<up> #2 + (b//#2) \<up> #2 = R \<up> #2]",
4.14 + "relations [A=#2*a*b - a \<up> #2, a=#2*R*sin alpha, b=#2*R*cos alpha]"];
4.15 val chkorg = map (the o (parse thy)) org;
4.16 val pbl = {given=["fixedValues [R=(R::real)]"],where_=[],
4.17 find=["maximum A", "values_for [a,b]"],
4.18 with_=[(* incompat.w. parse, ok with parseold
4.19 - "EX alpha. A=#2*a*b - a^^^#2 & \
4.20 + "EX alpha. A=#2*a*b - a \<up> #2 & \
4.21 \ a=#2*R*sin alpha & b=#2*R*cos alpha & \
4.22 - \ (ALL A'. A'=#2*a*b - a^^^#2 & a=#2*R*sin alpha \
4.23 + \ (ALL A'. A'=#2*a*b - a \<up> #2 & a=#2*R*sin alpha \
4.24 \ & b=#2*R*cos alpha \
4.25 \ --> A' <= A)"*)],
4.26 - relate=["relations [A=#2*a*b - a^^^#2, a=#2*R*sin alpha, b=#2*R*cos alpha]"]
4.27 + relate=["relations [A=#2*a*b - a \<up> #2, a=#2*R*sin alpha, b=#2*R*cos alpha]"]
4.28 }: string ppc;
4.29 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
4.30
4.31 @@ -72,10 +72,10 @@
4.32 find=["maximum A", "valuesFor [a=Undef]",
4.33 "function_term t", "max_argument mx"],
4.34 with_=[(* incompat.w. parse, ok with parseold
4.35 - "EX b alpha. A = #2*a*b - a^^^#2 & \
4.36 + "EX b alpha. A = #2*a*b - a \<up> #2 & \
4.37 \ a = #2*R*sin alpha & \
4.38 \ b = #2*R*cos alpha & \
4.39 - \ (ALL A'. A'= #2*a*b - a^^^#2 & \
4.40 + \ (ALL A'. A'= #2*a*b - a \<up> #2 & \
4.41 \ a = #2*R*sin alpha & \
4.42 \ b = #2*R*cos alpha --> A' <= A) & \
4.43 \ A = (%alpha. t) mx & \
4.44 @@ -85,7 +85,7 @@
4.45 "additionalRels ars"]}: string ppc;
4.46 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) met;
4.47
4.48 -val (SOME ct) = parseold thy "EX b. (EX alpha. A = #2*a*b - a^^^#2)";
4.49 +val (SOME ct) = parseold thy "EX b. (EX alpha. A = #2*a*b - a \<up> #2)";
4.50
4.51 "pbltyp --- make_fun ---";
4.52 (* subproblem [(hd #relate root, equality),
4.53 @@ -97,7 +97,7 @@
4.54 relate=[(*???*)]}: string ppc;
4.55 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
4.56 "coil";
4.57 -val pbl = {given=["equality (A=#2*a*b - a^^^#2)", "boundVariable alpha",
4.58 +val pbl = {given=["equality (A=#2*a*b - a \<up> #2)", "boundVariable alpha",
4.59 "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
4.60 where_=[],
4.61 find=["functionTerm t"],
4.62 @@ -131,7 +131,7 @@
4.63 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
4.64 "coil";
4.65 val pbl = {given=["functionTerm (f = #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \
4.66 - \ (#2*R*sin alpha)^^^#2)", "boundVariable alpha",
4.67 + \ (#2*R*sin alpha) \<up> #2)", "boundVariable alpha",
4.68 "domain {x::real. #0 <= x & x <= pi}"],where_=[],
4.69 find=["maximums [#1234]"],with_=[],relate=[]}: string ppc;
4.70 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
4.71 @@ -159,7 +159,7 @@
4.72 "p.117";
4.73 val org = {given=["[r=#5]"],where_=[],
4.74 find=["[x,(y::real)]"],with_=[],
4.75 - relate=["[is_max #0=pi*x^^^#2 + pi*x*(r::real)]"]}: string ppc;
4.76 + relate=["[is_max #0=pi*x \<up> #2 + pi*x*(r::real)]"]}: string ppc;
4.77 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
4.78 "#241";
4.79 val org = {given=["[s=(#10::real)]"],where_=[],
4.80 @@ -175,9 +175,9 @@
4.81 (* --- subproblem: derivative *)
4.82 (* --- subproblem: tan-quadrat-equation *)
4.83 "-------------- coil-kernel --------------";
4.84 -val origin = ["A=#2*a*b - a^^^#2",
4.85 +val origin = ["A=#2*a*b - a \<up> #2",
4.86 "a::real", "b::real", "{x. #0<x & x<R//#2}",
4.87 - "{(a//#2)^^^#2 + (b//#2)^^^#2 = (R//#2)^^^#2}",
4.88 + "{(a//#2) \<up> #2 + (b//#2) \<up> #2 = (R//#2) \<up> #2}",
4.89 "alpha::real", "{alpha::real. #0<alpha & alpha<pi//#2}",
4.90 "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",
4.91 "{R::real}"];
4.92 @@ -206,14 +206,14 @@
4.93
4.94 "------- 1.1 -------";
4.95 (* 5.3.00
4.96 -val formals = map (the o (parse thy)) ["A=#2*a*b - a^^^#2",
4.97 +val formals = map (the o (parse thy)) ["A=#2*a*b - a \<up> #2",
4.98 "a::real", "{x. #0<x & x<R//#2}",
4.99 - "{(a//#2)^^^#2 + (b//#2)^^^#2 = (R//#2)^^^#2}",
4.100 + "{(a//#2) \<up> #2 + (b//#2) \<up> #2 = (R//#2) \<up> #2}",
4.101 "{R::real}"];
4.102 val tag__forms = chktyps thy (formals, givens);
4.103 map ((atomty) o Thm.term_of) tag__forms;
4.104
4.105 -val formals = map (the o (parse thy)) ["A=#2*a*b - a^^^#2",
4.106 +val formals = map (the o (parse thy)) ["A=#2*a*b - a \<up> #2",
4.107 "alpha::real", "{alpha. #0<alpha & alpha<pi//#2}",
4.108 "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",
4.109 "{R::real}"];
4.110 @@ -222,7 +222,7 @@
4.111 *)
4.112
4.113 " --- subproblem: make-function-by-subst --- ";
4.114 -val origin = ["A=#2*a*b - a^^^#2",
4.115 +val origin = ["A=#2*a*b - a \<up> #2",
4.116 "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",
4.117 "{R::real}"];
4.118 val formals = map (the o (parse thy)) origin;
4.119 @@ -240,7 +240,7 @@
4.120 *)
4.121 " --- subproblem: max-of-function --- ";
4.122 val origin = ["A = #2*(#2*R*(sin alpha))*(#2*R*(sin alpha)) - \
4.123 - \ (#2*R*(sin alpha))^^^#2",
4.124 + \ (#2*R*(sin alpha)) \<up> #2",
4.125 "{alpha. #0<alpha & alpha<pi//#2}",
4.126 "{R::real}"];
4.127 val formals = map (the o (parse thy)) origin;
4.128 @@ -258,7 +258,7 @@
4.129 map ((atomty) o Thm.term_of) tag__forms;
4.130 *)
4.131 " --- subproblem: derivative --- ";
4.132 -val origin = ["x^^^#3-y^^^#3+#-3*x+#12*y+#10", "x::real"];
4.133 +val origin = ["x \<up> #3-y \<up> #3+#-3*x+#12*y+#10", "x::real"];
4.134 val formals = map (the o (parse thy)) origin;
4.135
4.136 val given = ["functionTerm t",
4.137 @@ -273,17 +273,17 @@
4.138 map ((atomty) o Thm.term_of) tag__forms;
4.139 *)
4.140 " --- subproblem: tan-quadrat-equation --- ";
4.141 -val origin = ["#8*R^^^#2*(cos alpha)^^^#2 + #-8*R^^^#2* \
4.142 - \ (cos alpha)*(sin alpha) + #8*R^^^#2*(sin alpha)^^^#2 = #0",
4.143 +val origin = ["#8*R \<up> #2*(cos alpha) \<up> #2 + #-8*R \<up> #2* \
4.144 + \ (cos alpha)*(sin alpha) + #8*R \<up> #2*(sin alpha) \<up> #2 = #0",
4.145 "alpha::real", "#1//#1000"];
4.146 val formals = map (the o (parse thy)) origin;
4.147
4.148 -val given = ["equation (a*(cos bdv)^^^#2 + b*(cos bdv)*(sin bdv) + \
4.149 +val given = ["equation (a*(cos bdv) \<up> #2 + b*(cos bdv)*(sin bdv) + \
4.150 \ c*(sin bdv) = #0)",
4.151 "boundVariable bdv", "errorBound epsilon"];
4.152 val where_ = ["bdv is_const", "epsilon is_const_expr"];
4.153 val find = ["L::real set"];
4.154 -val with_ = ["L = {x. || (%bdv. a*(cos bdv)^^^#2 + b*(cos bdv)*(sin bdv) + \
4.155 +val with_ = ["L = {x. || (%bdv. a*(cos bdv) \<up> #2 + b*(cos bdv)*(sin bdv) + \
4.156 \ c*(sin bdv)) x || < epsilon}"];
4.157 (* 5.3.00
4.158 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
4.159 @@ -310,10 +310,10 @@
4.160 "errorBound (eps = #1//#1000)",
4.161 "maximum A", "valuesFor [a=Undef]",
4.162 (*"functionTerm t", "max_argument mx",
4.163 - "max_relation (A=#2*a*b - a^^^#2)", *)
4.164 - "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
4.165 - "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
4.166 - "additionalRels [A=#2*a*b - a^^^#2,a=#2*R*sin alpha, b=#2*R*cos alpha]"];
4.167 + "max_relation (A=#2*a*b - a \<up> #2)", *)
4.168 + "additionalRels [A=#2*a*b - a \<up> #2,(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2]",
4.169 + "additionalRels [A=#2*a*b - a \<up> #2,(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2]",
4.170 + "additionalRels [A=#2*a*b - a \<up> #2,a=#2*R*sin alpha, b=#2*R*cos alpha]"];
4.171 val (dI',pI',mI')=
4.172 ("DiffAppl",["Program", "maximum_of", "function"],MethodC.id_empty);
4.173 val c = []:cid;
4.174 @@ -326,9 +326,9 @@
4.175 find=["maximum A", "valuesFor [a=Undef]"(*,
4.176 "functionTerm t", "max_argument mx"*)],
4.177 with_=[],
4.178 - relate=["max_relation (A=#2*a*b - a^^^#2)",
4.179 - "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
4.180 - "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
4.181 + relate=["max_relation (A=#2*a*b - a \<up> #2)",
4.182 + "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2]",
4.183 + "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2]",
4.184 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
4.185 }: string ppc;
4.186 *)
4.187 @@ -356,7 +356,7 @@
4.188 val ct = "max_relation ()";
4.189 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
4.190
4.191 -val ct = "relations [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]";
4.192 +val ct = "relations [A=#2*a*b - a \<up> #2,(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2]";
4.193 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
4.194
4.195 (* ... nxt = Specify_Domain ...
4.196 @@ -376,7 +376,7 @@
4.197 (* --- tricky case (termlist interleaving variants):
4.198 > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = Test_Code.CalcTreeTEST [(cts, (dI',pI',mI'))];
4.199
4.200 -> val ct = "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2, b=#2*R*cos alpha]";
4.201 +> val ct = "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2, b=#2*R*cos alpha]";
4.202 > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
4.203 *)
4.204
4.205 @@ -408,9 +408,9 @@
4.206 "errorBound (eps=#1//#1000)",
4.207 "maximum A", "valuesFor [a=Undef]",
4.208 (*"functionTerm t", "max_argument mx", *)
4.209 - "max_relation (A=#2*a*b - a^^^#2)",
4.210 - "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
4.211 - "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
4.212 + "max_relation (A=#2*a*b - a \<up> #2)",
4.213 + "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2]",
4.214 + "additionalRels [(a//#2) \<up> #2 + (b//#2) \<up> #2 =R \<up> #2]",
4.215 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"];
4.216 val (dI',pI',mI')=
4.217 ("DiffAppl",["DiffAppl", "test_maximum"],MethodC.id_empty);
5.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Sun Apr 25 12:03:49 2021 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Sun Apr 25 12:49:37 2021 +0200
5.3 @@ -17,7 +17,7 @@
5.4 antiDerivative :: "real => una"
5.5 antiDerivativeName :: "(real => real) => una"
5.6
5.7 - (*the CAS-command, eg. "Integrate (2*x^^^3, x)"*)
5.8 + (*the CAS-command, eg. "Integrate (2*x \<up> 3, x)"*)
5.9 Integrate :: "[real * real] => real"
5.10
5.11 axiomatization where
5.12 @@ -193,7 +193,7 @@
5.13 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
5.14
5.15 Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
5.16 - (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
5.17 + (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
5.18 ],
5.19 scr = Rule.Empty_Prog
5.20 }),
5.21 @@ -234,7 +234,7 @@
5.22 Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}),
5.23 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
5.24 Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*,
5.25 - (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
5.26 + (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
5.27 *****Rule.Thm ("add_divide_distrib",
5.28 ***** ThmC.numerals_to_Free @{thm add_divide_distrib})
5.29 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
5.30 @@ -287,7 +287,7 @@
5.31 * Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}),
5.32 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
5.33 * Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*,
5.34 -* (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
5.35 +* (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
5.36 * Rule.Thm ("add_divide_distrib",
5.37 * ThmC.numerals_to_Free @{thm add_divide_distrib})
5.38 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
6.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Sun Apr 25 12:03:49 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Sun Apr 25 12:49:37 2021 +0200
6.3 @@ -192,11 +192,11 @@
6.4 where
6.5 "partial_fraction f_f zzz = \<comment> \<open>([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))\<close>
6.6 (let f_f = Take f_f; \<comment> \<open>num_orig = 3\<close>
6.7 - num_orig = get_numerator f_f; \<comment> \<open>([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)\<close>
6.8 - f_f = (Rewrite_Set ''norm_Rational'') f_f; \<comment> \<open>denom = -1 + -2 * z + 8 * z ^^^ 2\<close>
6.9 - denom = get_denominator f_f; \<comment> \<open>equ = -1 + -2 * z + 8 * z ^^^ 2 = 0\<close>
6.10 + num_orig = get_numerator f_f; \<comment> \<open>([1], Res), 24 / (-1 + -2 * z + 8 * z \<up> 2)\<close>
6.11 + f_f = (Rewrite_Set ''norm_Rational'') f_f; \<comment> \<open>denom = -1 + -2 * z + 8 * z \<up> 2\<close>
6.12 + denom = get_denominator f_f; \<comment> \<open>equ = -1 + -2 * z + 8 * z \<up> 2 = 0\<close>
6.13 equ = denom = (0::real);
6.14 - \<comment> \<open>----- ([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)\<close>
6.15 + \<comment> \<open>----- ([2], Pbl), solve (-1 + -2 * z + 8 * z \<up> 2 = 0, z)\<close>
6.16 L_L = SubProblem (''Partial_Fractions'', \<comment> \<open>([2], Res), [z = 1 / 2, z = -1 / 4\<close>
6.17 [''abcFormula'', ''degree_2'', ''polynomial'', ''univariate'', ''equation''],
6.18 [''no_met'']) [BOOL equ, REAL zzz]; \<comment> \<open>facs: (z - 1 / 2) * (z - -1 / 4)\<close>
7.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sun Apr 25 12:03:49 2021 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Sun Apr 25 12:49:37 2021 +0200
7.3 @@ -110,7 +110,7 @@
7.4 real_minus_binom_pow3_p: "(a + -1 * b) \<up> 3 = a \<up> 3 + -3*a \<up> 2*b + 3*a*b \<up> 2 +
7.5 -1*b \<up> 3" and
7.6 (* real_plus_binom_pow: "[| n is_const; 3 < n |] ==>
7.7 - (a + b)^^^n = (a + b) * (a + b)\<up>(n - 1)" *)
7.8 + (a + b) \<up> n = (a + b) * (a + b)\<up>(n - 1)" *)
7.9 real_plus_binom_pow4: "(a + b) \<up> 4 = (a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3)
7.10 *(a + b)" and
7.11 real_plus_binom_pow4_poly: "[| a is_polyexp; b is_polyexp |] ==>
7.12 @@ -126,7 +126,7 @@
7.13 real_plus_binom_times: "(a + b)*(a + b) = a \<up> 2 + 2*a*b + b \<up> 2" and
7.14 real_minus_binom_times: "(a - b)*(a - b) = a \<up> 2 - 2*a*b + b \<up> 2" and
7.15 (*WN071229 changed for Schaerding -----vvv*)
7.16 - (*real_plus_binom_pow2: "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
7.17 + (*real_plus_binom_pow2: "(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)
7.18 real_plus_binom_pow2: "(a + b) \<up> 2 = (a + b) * (a + b)" and
7.19 (*WN071229 changed for Schaerding -----\<up>*)
7.20 real_plus_binom_pow2_poly: "[| a is_polyexp; b is_polyexp |] ==>
7.21 @@ -360,7 +360,7 @@
7.22
7.23 (* Gesamtgradordnung zum Vergleich von Monomen (Liste von Variablen/Potenzen):
7.24 zuerst nach Gesamtgrad, bei gleichem Gesamtgrad lexikographisch ordnen -
7.25 - dabei werden Koeffizienten ignoriert (2*3*a^^^2*4*b gilt wie a^^^2*b) *)
7.26 + dabei werden Koeffizienten ignoriert (2*3*a \<up> 2*4*b gilt wie a \<up> 2*b) *)
7.27 fun degree_ord (xs, ys) =
7.28 prod_ord int_ord (dict_cond_ord var_ord_revPow is_nums)
7.29 ((monom_degree xs, xs), (monom_degree ys, ys));
7.30 @@ -694,20 +694,20 @@
7.31 calc = [], errpatts = [],
7.32 rules =
7.33 [Rule.Thm ("real_plus_binom_pow4", ThmC.numerals_to_Free @{thm real_plus_binom_pow4}),
7.34 - (*"(a + b)^^^4 = ... "*)
7.35 + (*"(a + b) \<up> 4 = ... "*)
7.36 Rule.Thm ("real_plus_binom_pow5",ThmC.numerals_to_Free @{thm real_plus_binom_pow5}),
7.37 - (*"(a + b)^^^5 = ... "*)
7.38 + (*"(a + b) \<up> 5 = ... "*)
7.39 Rule.Thm ("real_plus_binom_pow3",ThmC.numerals_to_Free @{thm real_plus_binom_pow3}),
7.40 - (*"(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
7.41 + (*"(a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3" *)
7.42 (*WN071229 changed/removed for Schaerding -----vvv*)
7.43 (*Rule.Thm ("real_plus_binom_pow2",ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),*)
7.44 - (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
7.45 + (*"(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)
7.46 Rule.Thm ("real_plus_binom_pow2",ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
7.47 - (*"(a + b)^^^2 = (a + b) * (a + b)"*)
7.48 + (*"(a + b) \<up> 2 = (a + b) * (a + b)"*)
7.49 (*Rule.Thm ("real_plus_minus_binom1_p_p", ThmC.numerals_to_Free @{thm real_plus_minus_binom1_p_p}),*)
7.50 - (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
7.51 + (*"(a + b)*(a + -1 * b) = a \<up> 2 + -1*b \<up> 2"*)
7.52 (*Rule.Thm ("real_plus_minus_binom2_p_p", ThmC.numerals_to_Free @{thm real_plus_minus_binom2_p_p}),*)
7.53 - (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
7.54 + (*"(a + -1 * b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
7.55 (*WN071229 changed/removed for Schaerding -----\<up>*)
7.56
7.57 Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
7.58 @@ -731,19 +731,19 @@
7.59 calc = [], errpatts = [],
7.60 rules =
7.61 [Rule.Thm ("real_plus_binom_pow4_poly", ThmC.numerals_to_Free @{thm real_plus_binom_pow4_poly}),
7.62 - (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^4 = ... "*)
7.63 + (*"[| a is_polyexp; b is_polyexp |] ==> (a + b) \<up> 4 = ... "*)
7.64 Rule.Thm ("real_plus_binom_pow5_poly", ThmC.numerals_to_Free @{thm real_plus_binom_pow5_poly}),
7.65 - (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^5 = ... "*)
7.66 + (*"[| a is_polyexp; b is_polyexp |] ==> (a + b) \<up> 5 = ... "*)
7.67 Rule.Thm ("real_plus_binom_pow2_poly",ThmC.numerals_to_Free @{thm real_plus_binom_pow2_poly}),
7.68 (*"[| a is_polyexp; b is_polyexp |] ==>
7.69 - (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
7.70 + (a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)
7.71 Rule.Thm ("real_plus_binom_pow3_poly",ThmC.numerals_to_Free @{thm real_plus_binom_pow3_poly}),
7.72 (*"[| a is_polyexp; b is_polyexp |] ==>
7.73 - (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
7.74 + (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3" *)
7.75 Rule.Thm ("real_plus_minus_binom1_p_p",ThmC.numerals_to_Free @{thm real_plus_minus_binom1_p_p}),
7.76 - (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
7.77 + (*"(a + b)*(a + -1 * b) = a \<up> 2 + -1*b \<up> 2"*)
7.78 Rule.Thm ("real_plus_minus_binom2_p_p",ThmC.numerals_to_Free @{thm real_plus_minus_binom2_p_p}),
7.79 - (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
7.80 + (*"(a + -1 * b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
7.81
7.82 Rule.Thm ("real_add_mult_distrib_poly",
7.83 ThmC.numerals_to_Free @{thm real_add_mult_distrib_poly}),
7.84 @@ -765,7 +765,7 @@
7.85 erls = Rule_Set.empty, srls = Rule_Set.Empty,
7.86 calc = [], errpatts = [],
7.87 rules = [(*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
7.88 - a*(a*a) --> a*a^^^2 und nicht a*(a*a) --> a^^^2*a *)
7.89 + a*(a*a) --> a*a \<up> 2 und nicht a*(a*a) --> a \<up> 2*a *)
7.90 Rule.Thm ("sym_realpow_twoI",
7.91 ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
7.92 (*"r * r = r \<up> 2"*)
7.93 @@ -777,7 +777,7 @@
7.94 Rule.Thm ("realpow_plus_1_assoc_l",
7.95 ThmC.numerals_to_Free @{thm realpow_plus_1_assoc_l}),
7.96 (*"r * (r \<up> m * s) = r \<up> (1 + m) * s"*)
7.97 - (*MG 9.7.03: neues Rule.Thm wegen a*(a*(a*b)) --> a^^^2*(a*b) *)
7.98 + (*MG 9.7.03: neues Rule.Thm wegen a*(a*(a*b)) --> a \<up> 2*(a*b) *)
7.99 Rule.Thm ("realpow_plus_1_assoc_l2",
7.100 ThmC.numerals_to_Free @{thm realpow_plus_1_assoc_l2}),
7.101 (*"r \<up> m * (r * s) = r \<up> (1 + m) * s"*)
7.102 @@ -789,7 +789,7 @@
7.103 (*"r \<up> n * (r \<up> m * s) = r \<up> (n + m) * s"*)
7.104
7.105 (* ist in expand_poly - wird hier aber auch gebraucht, wegen:
7.106 - "r * r = r \<up> 2" wenn r=a^^^b*)
7.107 + "r * r = r \<up> 2" wenn r=a \<up> b*)
7.108 Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow})
7.109 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
7.110 ], scr = Rule.Empty_Prog};
7.111 @@ -815,9 +815,9 @@
7.112 calc = [], errpatts = [],
7.113 rules = [(* MG: folgende Rule.Thm müssen hier stehen bleiben: *)
7.114 Rule.Thm ("mult_1_right",ThmC.numerals_to_Free @{thm mult_1_right}),
7.115 - (*"z * 1 = z"*) (*wegen "a * b * b^^^(-1) + a"*)
7.116 + (*"z * 1 = z"*) (*wegen "a * b * b \<up> (-1) + a"*)
7.117 Rule.Thm ("realpow_zeroI",ThmC.numerals_to_Free @{thm realpow_zeroI}),
7.118 - (*"r \<up> 0 = 1"*) (*wegen "a*a^^^(-1)*c + b + c"*)
7.119 + (*"r \<up> 0 = 1"*) (*wegen "a*a \<up> (-1)*c + b + c"*)
7.120 Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI}),
7.121 (*"r \<up> 1 = r"*)
7.122 Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI})
7.123 @@ -896,15 +896,15 @@
7.124 ....... 18.3.03 undefined???*)
7.125
7.126 Rule.Thm ("real_plus_binom_pow2",ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
7.127 - (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
7.128 + (*"(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)
7.129 Rule.Thm ("real_minus_binom_pow2_p",ThmC.numerals_to_Free @{thm real_minus_binom_pow2_p}),
7.130 - (*"(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"*)
7.131 + (*"(a - b) \<up> 2 = a \<up> 2 + -2*a*b + b \<up> 2"*)
7.132 Rule.Thm ("real_plus_minus_binom1_p",
7.133 ThmC.numerals_to_Free @{thm real_plus_minus_binom1_p}),
7.134 - (*"(a + b)*(a - b) = a^^^2 + -1*b^^^2"*)
7.135 + (*"(a + b)*(a - b) = a \<up> 2 + -1*b \<up> 2"*)
7.136 Rule.Thm ("real_plus_minus_binom2_p",
7.137 ThmC.numerals_to_Free @{thm real_plus_minus_binom2_p}),
7.138 - (*"(a - b)*(a + b) = a^^^2 + -1*b^^^2"*)
7.139 + (*"(a - b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
7.140
7.141 Rule.Thm ("minus_minus",ThmC.numerals_to_Free @{thm minus_minus}),
7.142 (*"- (- ?z) = ?z"*)
7.143 @@ -1204,9 +1204,9 @@
7.144 rules = [Rule.Thm ("real_plus_binom_times" ,ThmC.numerals_to_Free @{thm real_plus_binom_times}),
7.145 (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
7.146 Rule.Thm ("real_plus_binom_times1" ,ThmC.numerals_to_Free @{thm real_plus_binom_times1}),
7.147 - (*"(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"*)
7.148 + (*"(a + 1*b)*(a + -1*b) = a \<up> 2 + -1*b \<up> 2"*)
7.149 Rule.Thm ("real_plus_binom_times2" ,ThmC.numerals_to_Free @{thm real_plus_binom_times2}),
7.150 - (*"(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"*)
7.151 + (*"(a + -1*b)*(a + 1*b) = a \<up> 2 + -1*b \<up> 2"*)
7.152
7.153 Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),(*"1 * z = z"*)
7.154
7.155 @@ -1331,12 +1331,12 @@
7.156 Rule.Thm ("real_mm_binom_times",ThmC.numerals_to_Free @{thm real_mm_binom_times}),
7.157 (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
7.158 Rule.Thm ("realpow_multI",ThmC.numerals_to_Free @{thm realpow_multI}),
7.159 - (*(a*b)^^^n = a^^^n * b^^^n*)
7.160 + (*(a*b) \<up> n = a \<up> n * b \<up> n*)
7.161 Rule.Thm ("real_plus_binom_pow3",ThmC.numerals_to_Free @{thm real_plus_binom_pow3}),
7.162 - (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
7.163 + (* (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3 *)
7.164 Rule.Thm ("real_minus_binom_pow3",
7.165 ThmC.numerals_to_Free @{thm real_minus_binom_pow3}),
7.166 - (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
7.167 + (* (a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3 *)
7.168
7.169
7.170 (*Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
8.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Sun Apr 25 12:03:49 2021 +0200
8.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Sun Apr 25 12:49:37 2021 +0200
8.3 @@ -144,7 +144,7 @@
8.4 Rule.Thm("real_rat_mult_3",ThmC.numerals_to_Free @{thm real_rat_mult_3}),
8.5 (* (a/b)*c = (a*c)/b*)
8.6 Rule.Thm("real_rat_pow",ThmC.numerals_to_Free @{thm real_rat_pow}),
8.7 - (*(a/b)^^^2 = a^^^2/b^^^2*)
8.8 + (*(a/b) \<up> 2 = a \<up> 2/b \<up> 2*)
8.9 Rule.Thm("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
8.10 (* a - b = a + (-1) * b *)
8.11 Rule.Thm("rat_double_rat_1",ThmC.numerals_to_Free @{thm rat_double_rat_1}),
9.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml Sun Apr 25 12:03:49 2021 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml Sun Apr 25 12:49:37 2021 +0200
9.3 @@ -86,21 +86,21 @@
9.4 term2poly t v;
9.5 val t = (Thm.term_of o the o (parse thy)) "#1 * x::real"; (*FIXME: drop it*)
9.6 term2poly t v;
9.7 -val t = (Thm.term_of o the o (parse thy)) "x^^^#1"; (*FIXME: drop it*)
9.8 +val t = (Thm.term_of o the o (parse thy)) "x \<up> #1"; (*FIXME: drop it*)
9.9 term2poly t v;
9.10 -val t = (Thm.term_of o the o (parse thy)) "x^^^#3";
9.11 +val t = (Thm.term_of o the o (parse thy)) "x \<up> #3";
9.12 term2poly t v;
9.13 -val t = (Thm.term_of o the o (parse thy)) "#3 * x^^^#3";
9.14 +val t = (Thm.term_of o the o (parse thy)) "#3 * x \<up> #3";
9.15 term2poly t v;
9.16 -val t = (Thm.term_of o the o (parse thy)) "#-1 + #3 * x^^^#3";
9.17 +val t = (Thm.term_of o the o (parse thy)) "#-1 + #3 * x \<up> #3";
9.18 term2poly t v;
9.19 -val t = (Thm.term_of o the o (parse thy)) "#-1 + (#3 * x^^^#3 + #5 * x^^^#5)";
9.20 +val t = (Thm.term_of o the o (parse thy)) "#-1 + (#3 * x \<up> #3 + #5 * x \<up> #5)";
9.21 term2poly t v;
9.22 val t = (Thm.term_of o the o (parse thy))
9.23 - "#-1 + (#3 * x^^^#3 + (#5 * x^^^#5 + #7 * x^^^#7))";
9.24 + "#-1 + (#3 * x \<up> #3 + (#5 * x \<up> #5 + #7 * x \<up> #7))";
9.25 term2poly t v;
9.26 val t = (Thm.term_of o the o (parse thy))
9.27 - "#3 * x^^^#3 + (#5 * x^^^#5 + #7 * x^^^#7)";
9.28 + "#3 * x \<up> #3 + (#5 * x \<up> #5 + #7 * x \<up> #7)";
9.29 term2poly t v;
9.30
9.31
10.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sun Apr 25 12:03:49 2021 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Sun Apr 25 12:49:37 2021 +0200
10.3 @@ -436,7 +436,7 @@
10.4 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
10.5
10.6 Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power}),
10.7 - (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
10.8 + (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
10.9
10.10 Rule.Thm ("mult_cross", ThmC.numerals_to_Free @{thm mult_cross}),
10.11 (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)
10.12 @@ -618,29 +618,29 @@
10.13 Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
10.14 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
10.15 rules = [Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}),
10.16 - (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
10.17 + (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
10.18 Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow}),
10.19 - (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
10.20 + (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
10.21 Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI}),
10.22 - (*"r ^^^ 1 = r"*)
10.23 + (*"r \<up> 1 = r"*)
10.24 Rule.Thm ("realpow_minus_even",ThmC.numerals_to_Free @{thm realpow_minus_even}),
10.25 - (*"n is_even ==> (- r) ^^^ n = r ^^^ n" ?-->discard_minus?*)
10.26 + (*"n is_even ==> (- r) \<up> n = r \<up> n" ?-->discard_minus?*)
10.27 Rule.Thm ("realpow_minus_odd",ThmC.numerals_to_Free @{thm realpow_minus_odd}),
10.28 - (*"Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"*)
10.29 + (*"Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*)
10.30
10.31 (*----- collect atoms over * -----*)
10.32 Rule.Thm ("realpow_two_atom",ThmC.numerals_to_Free @{thm realpow_two_atom}),
10.33 - (*"r is_atom ==> r * r = r ^^^ 2"*)
10.34 + (*"r is_atom ==> r * r = r \<up> 2"*)
10.35 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
10.36 - (*"r is_atom ==> r * r ^^^ n = r ^^^ (n + 1)"*)
10.37 + (*"r is_atom ==> r * r \<up> n = r \<up> (n + 1)"*)
10.38 Rule.Thm ("realpow_addI_atom",ThmC.numerals_to_Free @{thm realpow_addI_atom}),
10.39 - (*"r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
10.40 + (*"r is_atom ==> r \<up> n * r \<up> m = r \<up> (n + m)"*)
10.41
10.42 (*----- distribute none-atoms -----*)
10.43 Rule.Thm ("realpow_def_atom",ThmC.numerals_to_Free @{thm realpow_def_atom}),
10.44 - (*"[| 1 < n; not(r is_atom) |]==>r ^^^ n = r * r ^^^ (n + -1)"*)
10.45 + (*"[| 1 < n; not(r is_atom) |]==>r \<up> n = r * r \<up> (n + -1)"*)
10.46 Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI}),
10.47 - (*"1 ^^^ n = 1"*)
10.48 + (*"1 \<up> n = 1"*)
10.49 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
10.50 ],
10.51 scr = Rule.Empty_Prog
10.52 @@ -656,8 +656,8 @@
10.53 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
10.54 otherwise inv.to a / b / c = ...*)
10.55 Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left}),
10.56 - (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x^^^n too much
10.57 - and does not commute a / b * c ^^^ 2 !*)
10.58 + (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x \<up> n too much
10.59 + and does not commute a / b * c \<up> 2 !*)
10.60
10.61 Rule.Thm ("divide_divide_eq_right",
10.62 ThmC.numerals_to_Free @{thm divide_divide_eq_right}),
10.63 @@ -810,7 +810,7 @@
10.64 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
10.65
10.66 Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
10.67 - (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
10.68 + (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
10.69 ],
10.70 scr = Rule.Empty_Prog});
10.71
11.1 --- a/src/Tools/isac/Knowledge/Root.thy Sun Apr 25 12:03:49 2021 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Root.thy Sun Apr 25 12:49:37 2021 +0200
11.3 @@ -227,9 +227,9 @@
11.4
11.5 Rule.Thm ("sym_realpow_twoI",
11.6 ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
11.7 - (*"r1 * r1 = r1 ^^^ 2"*)
11.8 + (*"r1 * r1 = r1 \<up> 2"*)
11.9 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
11.10 - (*"r * r ^^^ n = r ^^^ (n + 1)"*)
11.11 + (*"r * r \<up> n = r \<up> (n + 1)"*)
11.12 Rule.Thm ("sym_real_mult_2",
11.13 ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
11.14 (*"z1 + z1 = 2 * z1"*)
11.15 @@ -264,17 +264,17 @@
11.16 erls = Atools_erls, srls = Rule_Set.Empty,
11.17 calc = [], errpatts = [],
11.18 rules = [Rule.Thm ("real_plus_binom_pow2" ,ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
11.19 - (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
11.20 + (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
11.21 Rule.Thm ("real_plus_binom_times" ,ThmC.numerals_to_Free @{thm real_plus_binom_times}),
11.22 (*"(a + b)*(a + b) = ...*)
11.23 Rule.Thm ("real_minus_binom_pow2" ,ThmC.numerals_to_Free @{thm real_minus_binom_pow2}),
11.24 - (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
11.25 + (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*)
11.26 Rule.Thm ("real_minus_binom_times",ThmC.numerals_to_Free @{thm real_minus_binom_times}),
11.27 (*"(a - b)*(a - b) = ...*)
11.28 Rule.Thm ("real_plus_minus_binom1",ThmC.numerals_to_Free @{thm real_plus_minus_binom1}),
11.29 - (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
11.30 + (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*)
11.31 Rule.Thm ("real_plus_minus_binom2",ThmC.numerals_to_Free @{thm real_plus_minus_binom2}),
11.32 - (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
11.33 + (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)
11.34 (*RL 020915*)
11.35 Rule.Thm ("real_pp_binom_times",ThmC.numerals_to_Free @{thm real_pp_binom_times}),
11.36 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
11.37 @@ -285,7 +285,7 @@
11.38 Rule.Thm ("real_mm_binom_times",ThmC.numerals_to_Free @{thm real_mm_binom_times}),
11.39 (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
11.40 Rule.Thm ("realpow_mul",ThmC.numerals_to_Free @{thm realpow_mul}),
11.41 - (*(a*b)^^^n = a^^^n * b^^^n*)
11.42 + (*(a*b) \<up> n = a \<up> n * b \<up> n*)
11.43
11.44 Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}), (*"1 * z = z"*)
11.45 Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}), (*"0 * z = 0"*)
11.46 @@ -301,9 +301,9 @@
11.47
11.48 Rule.Thm ("sym_realpow_twoI",
11.49 ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
11.50 - (*"r1 * r1 = r1 ^^^ 2"*)
11.51 + (*"r1 * r1 = r1 \<up> 2"*)
11.52 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
11.53 - (*"r * r ^^^ n = r ^^^ (n + 1)"*)
11.54 + (*"r * r \<up> n = r \<up> (n + 1)"*)
11.55 Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
11.56 (*"z1 + (z1 + k) = 2 * z1 + k"*)
11.57
12.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Sun Apr 25 12:03:49 2021 +0200
12.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Sun Apr 25 12:49:37 2021 +0200
12.3 @@ -218,9 +218,9 @@
12.4 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
12.5 rules = [
12.6 Rule.Thm("sqrt_square_1",ThmC.numerals_to_Free @{thm sqrt_square_1}),
12.7 - (* (sqrt a)^^^2 -> a *)
12.8 + (* (sqrt a) \<up> 2 -> a *)
12.9 Rule.Thm("sqrt_square_2",ThmC.numerals_to_Free @{thm sqrt_square_2}),
12.10 - (* sqrt (a^^^2) -> a *)
12.11 + (* sqrt (a \<up> 2) -> a *)
12.12 Rule.Thm("sqrt_times_root_1",ThmC.numerals_to_Free @{thm sqrt_times_root_1}),
12.13 (* sqrt a sqrt b -> sqrt(ab) *)
12.14 Rule.Thm("sqrt_times_root_2",ThmC.numerals_to_Free @{thm sqrt_times_root_2}),
12.15 @@ -318,9 +318,9 @@
12.16 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
12.17 rules = [
12.18 Rule.Thm("sqrt_square_1",ThmC.numerals_to_Free @{thm sqrt_square_1}),
12.19 - (* (sqrt a)^^^2 -> a *)
12.20 + (* (sqrt a) \<up> 2 -> a *)
12.21 Rule.Thm("sqrt_square_2",ThmC.numerals_to_Free @{thm sqrt_square_2}),
12.22 - (* sqrt (a^^^2) -> a *)
12.23 + (* sqrt (a \<up> 2) -> a *)
12.24 Rule.Thm("sqrt_times_root_1",ThmC.numerals_to_Free @{thm sqrt_times_root_1}),
12.25 (* sqrt a sqrt b -> sqrt(ab) *)
12.26 Rule.Thm("sqrt_times_root_2",ThmC.numerals_to_Free @{thm sqrt_times_root_2}),
12.27 @@ -364,9 +364,9 @@
12.28 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
12.29 rules = [
12.30 Rule.Thm("sqrt_square_1",ThmC.numerals_to_Free @{thm sqrt_square_1}),
12.31 - (* (sqrt a)^^^2 -> a *)
12.32 + (* (sqrt a) \<up> 2 -> a *)
12.33 Rule.Thm("sqrt_square_2",ThmC.numerals_to_Free @{thm sqrt_square_2}),
12.34 - (* sqrt (a^^^2) -> a *)
12.35 + (* sqrt (a \<up> 2) -> a *)
12.36 Rule.Thm("sqrt_times_root_1",ThmC.numerals_to_Free @{thm sqrt_times_root_1}),
12.37 (* sqrt a sqrt b -> sqrt(ab) *)
12.38 Rule.Thm("sqrt_times_root_2",ThmC.numerals_to_Free @{thm sqrt_times_root_2}),
12.39 @@ -426,9 +426,9 @@
12.40 Rule.Thm("sqrt_times_root_2",ThmC.numerals_to_Free @{thm sqrt_times_root_2}),
12.41 (* a * sqrt a * sqrt b = a * sqrt(a*b) *)
12.42 Rule.Thm("sqrt_square_2",ThmC.numerals_to_Free @{thm sqrt_square_2}),
12.43 - (* sqrt (a^^^2) = a *)
12.44 + (* sqrt (a \<up> 2) = a *)
12.45 Rule.Thm("sqrt_square_1",ThmC.numerals_to_Free @{thm sqrt_square_1})
12.46 - (* sqrt a ^^^ 2 = a *)
12.47 + (* sqrt a \<up> 2 = a *)
12.48 ],
12.49 scr = Rule.Empty_Prog
12.50 });
13.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Sun Apr 25 12:03:49 2021 +0200
13.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Sun Apr 25 12:49:37 2021 +0200
13.3 @@ -170,7 +170,7 @@
13.4 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
13.5 ----- before ?patterns ---:
13.6 > val t = (Thm.term_of o the o (parse thy))
13.7 - "matches (a * b^^^#2 = c) (#3 * x^^^#2 = #1)";
13.8 + "matches (a * b \<up> #2 = c) (#3 * x \<up> #2 = #1)";
13.9 > eval_matches "/thmid/" "/op_/" t thy;
13.10 SOME
13.11 ("matches (a * b \<up> #2 = c) (#3 * x \<up> #2 = #1) = True",
13.12 @@ -178,7 +178,7 @@
13.13 : (string * term) option
13.14
13.15 > val t = (Thm.term_of o the o (parse thy))
13.16 - "matches (a * b^^^#2 = c) (#3 * x^^^#2222 = #1)";
13.17 + "matches (a * b \<up> #2 = c) (#3 * x \<up> #2222 = #1)";
13.18 > eval_matches "/thmid/" "/op_/" t thy;
13.19 SOME ("matches (a * b \<up> #2 = c) (#3 * x \<up> #2222 = #1) = False",
13.20 Const ("HOL.Trueprop", "bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
14.1 --- a/test/Tools/isac/Test_Some.thy Sun Apr 25 12:03:49 2021 +0200
14.2 +++ b/test/Tools/isac/Test_Some.thy Sun Apr 25 12:49:37 2021 +0200
14.3 @@ -91,117 +91,17 @@
14.4 declare [[ML_exception_trace]]
14.5 \<close>
14.6
14.7 -section \<open>====== ML_file "MathEngBasic/thmC.sml" ============================================\<close>
14.8 +section \<open>===================================================================================\<close>
14.9 ML \<open>
14.10 \<close> ML \<open>
14.11 -"----------- fun revert_sym_rule ---------------------------------------------------------------";
14.12 -"----------- fun revert_sym_rule ---------------------------------------------------------------";
14.13 -"----------- fun revert_sym_rule ---------------------------------------------------------------";
14.14 -"~~~~~ fun revert_sym_rule , args:"; val (thy, (Rule.Thm (id, thm))) =
14.15 - (@{theory Isac_Knowledge},
14.16 - Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})));
14.17 -
14.18 -if id = "sym_real_mult_minus1" andalso ThmC.string_of_thm thm = "- ?z1 = -1 * ?z1" then ()
14.19 -else error "input to revert_sym_rule CHANGED";
14.20 -
14.21 -\<close> ML \<open>
14.22 - (*if*) is_sym (cut_id id) (*then*);
14.23 -\<close> ML \<open>
14.24 - val id' = id_drop_sym id
14.25 -\<close> ML \<open>
14.26 - val thm' = thm_from_thy thy id'
14.27 -\<close> ML \<open>
14.28 - val id'' = Thm.get_name_hint thm'
14.29 -\<close> ML \<open>
14.30 -val thy = @{theory Isac_Knowledge}
14.31 -val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
14.32 - (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})))
14.33 -;
14.34 -if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "-1 * ?z = - ?z"
14.35 -then () else error "fun revert_sym_rule changed 1";
14.36 -
14.37 -val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
14.38 - (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))
14.39 -;
14.40 -if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + -1 * ?b"
14.41 -then () else error "fun revert_sym_rule changed 2"
14.42 -\<close> ML \<open>
14.43 -\<close> ML \<open>
14.44 -\<close> ML \<open>
14.45 -\<close> ML \<open>
14.46 -\<close> ML \<open>
14.47 -\<close> ML \<open>
14.48 -\<close> ML \<open>
14.49 \<close> ML \<open>
14.50 \<close> ML \<open>
14.51 \<close>
14.52
14.53 -section \<open>=========== ML_file "BridgeLibisabelle/thy-hierarchy.sml" ======================\<close>
14.54 +section \<open>===================================================================================\<close>
14.55 ML \<open>
14.56 \<close> ML \<open>
14.57 \<close> ML \<open>
14.58 -"----------- fun ThmC_Def.make_thm ------------------------------------";
14.59 -"----------- fun ThmC_Def.make_thm ------------------------------------";
14.60 -"----------- fun ThmC_Def.make_thm ------------------------------------";
14.61 -"~~~~~ fun ThmC_Def.make_thm, args:"; val (thy, part, (thmID : ThmC.id, thm), (mathauthors : Thy_Write.authors)) =
14.62 - (@{theory "Biegelinie"}, "IsacKnowledge",
14.63 - ("Belastung_Querkraft", Thm.prop_of @{thm Belastung_Querkraft}),
14.64 - ["Walther Neuper 2005 supported by a grant from NMI Austria"]);
14.65 - val guh = Thy_Write.thm2guh (part, Context.theory_name thy) thmID
14.66 - val theID = Thy_Present.guh2theID guh;
14.67 -if guh = "thy_isac_Biegelinie-thm-Belastung_Querkraft" andalso
14.68 - theID = ["IsacKnowledge", "Biegelinie", "Theorems", "Belastung_Querkraft"]
14.69 -then () else error "store_thm: guh | theID changed";
14.70 -
14.71 -\<close> ML \<open> (*ERROR "??.unknown"*)
14.72 -"----------- fun thms_of_rlss ------------------------------------";
14.73 -"----------- fun thms_of_rlss ------------------------------------";
14.74 -"----------- fun thms_of_rlss ------------------------------------";
14.75 -\<close> ML \<open>
14.76 -val rlss =
14.77 - [("empty" : Rule_Set.id, ("Know_Store": ThyC.id, Rule_Set.empty)),
14.78 - ("discard_minus" : Rule_Set.id, ("Poly": ThyC.id, discard_minus))]:
14.79 - (id * (id * Rule_Def.rule_set)) list
14.80 -;
14.81 -\<close> ML \<open>
14.82 -(*--- fun ThmC_Def.make_thm --- avoids ERROR BELOW Undefined fact: "real_mult_minus1"*)
14.83 -(*+*)thms_of_rlss thy rlss (* = [("??.unknown", "?a - ?b = ?a + -1 * ?b")]: (string * thm) list*)
14.84 -\<close> ML \<open>
14.85 -(*+*)Rule_Set.empty: Rule_Def.rule_set
14.86 -\<close> ML \<open>
14.87 -(*+*)discard_minus: Rule_Def.rule_set
14.88 -\<close> ML \<open>
14.89 -val [_, (thmID, term)] = thms_of_rlss thy rlss;
14.90 -
14.91 -\<close> ML \<open>
14.92 -if thmID = "real_mult_minus1" (* WAS "??.unknown" *)
14.93 -then () else error "thms_of_rlss changed";
14.94 -
14.95 -\<close> ML \<open>
14.96 -"~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac_Knowledge}, rlss);
14.97 -val rlss' = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
14.98 - |> map (Thy_Hierarchy.thms_of_rls o #2 o #2)
14.99 - (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
14.100 - Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*)
14.101 - |> flat
14.102 - (* = [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
14.103 - Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]*)
14.104 - |> map (ThmC.revert_sym_rule thy)
14.105 - (* = [Thm ("Poly.real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
14.106 - Thm ("Delete.real_mult_minus1", "-1 * ?z = - ?z")] : rule list*)
14.107 - |> map (fn Thm (thmID, thm) => (thmID, Thm.prop_of thm))
14.108 - (* = [("Poly.real_diff_minus", Const ("HOL.Trueprop", "bool \<Rightarrow> prop") $ ...,
14.109 - ("Delete.real_mult_minus1", Const ("HOL.Trueprop", ...)] : (string * term) list*)
14.110 - |> distinct (fn ((thmID1, thm1), (thmID2, thm2)) => thmID1 = thmID2);
14.111 -\<close> ML \<open>
14.112 -\<close> ML \<open>
14.113 -\<close> ML \<open>
14.114 -\<close> ML \<open>
14.115 -\<close> ML \<open>
14.116 -\<close> ML \<open>
14.117 -\<close> ML \<open>
14.118 -\<close> ML \<open>
14.119 -\<close> ML \<open>
14.120 \<close> ML \<open>
14.121 \<close>
14.122