1.1 --- a/TODO.md Sun May 02 15:55:37 2021 +0200
1.2 +++ b/TODO.md Mon May 03 08:49:50 2021 +0200
1.3 @@ -28,8 +28,6 @@
1.4 - sometimes this requires to use more specific types / type classes;
1.5 - sometimes this requires to use proper definitional mechanisms (e.g. 'primrec', 'fun');
1.6 - a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation);
1.7 - - abbreviation real_powr :: "real \<Rightarrow> real \<Rightarrow> real" (infixr "\<up>" 80)
1.8 - where "x \<up> a \<equiv> x powr a"
1.9
1.10 * WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation
1.11 - clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Sun May 02 15:55:37 2021 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Mon May 03 08:49:50 2021 +0200
2.3 @@ -577,7 +577,7 @@
2.4 val poly_consts = (* TODO: adopt syntax-const from Isabelle*)
2.5 ["Groups.plus_class.plus", "Groups.minus_class.minus",
2.6 "Rings.divide_class.divide", "Groups.times_class.times",
2.7 - "Prog_Expr.pow"];
2.8 + "Transcendental.powr"];
2.9 (* treat Free, Const, Var as variables in polynomials *)
2.10 fun vars_of t =
2.11 let
3.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Sun May 02 15:55:37 2021 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Mon May 03 08:49:50 2021 +0200
3.3 @@ -38,7 +38,7 @@
3.4 ("MINUS", ("Groups.minus_class.minus", (**)eval_binop "#sub_")),
3.5 ("TIMES", ("Groups.times_class.times", (**)eval_binop "#mult_")),
3.6 ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
3.7 - ("POWER",("Prog_Expr.pow", (**)eval_binop "#power_")),
3.8 + ("POWER",("Transcendental.powr", (**)eval_binop "#power_")),
3.9 ("boollist2sum", ("Prog_Expr.boollist2sum", Prog_Expr.eval_boollist2sum ""))]\<close>
3.10
3.11 subsection \<open>rewrite-order for rule-sets\<close>
4.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Sun May 02 15:55:37 2021 +0200
4.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Mon May 03 08:49:50 2021 +0200
4.3 @@ -49,7 +49,7 @@
4.4 (*
4.5 Don't use
4.6 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
4.7 - Rule.Eval ("Prog_Expr.pow" , (**)eval_binop "#power_"),
4.8 + Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_"),
4.9 *)
4.10 ];
4.11
4.12 @@ -60,7 +60,7 @@
4.13 (*
4.14 Don't use
4.15 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
4.16 - Rule.Eval ("Prog_Expr.pow" , (**)eval_binop "#power_"),
4.17 + Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_"),
4.18 *)
4.19 ];
4.20 \<close>
4.21 @@ -83,7 +83,7 @@
4.22 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
4.23 Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_"),
4.24 *)
4.25 - Rule.Eval ("Prog_Expr.pow" , (**)eval_binop "#power_")
4.26 + Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_")
4.27 ],
4.28 scr = Rule.Empty_Prog});
4.29 \<close>
5.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sun May 02 15:55:37 2021 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Mon May 03 08:49:50 2021 +0200
5.3 @@ -180,7 +180,7 @@
5.4 val poly_consts =
5.5 ["Groups.plus_class.plus", "Groups.minus_class.minus",
5.6 "Rings.divide_class.divide", "Groups.times_class.times",
5.7 - "Prog_Expr.pow"];
5.8 + "Transcendental.powr"];
5.9 \<close>
5.10 subsubsection \<open>for predicates in specifications (ML)\<close>
5.11 ML \<open>
5.12 @@ -190,9 +190,9 @@
5.13 if (1) then degree 0
5.14 if (2) then v is a factor on the very right, ev. with exponent.*)
5.15 fun factor_right_deg (*case 2*)
5.16 - (Const ("Groups.times_class.times", _) $ t1 $ (Const ("Prog_Expr.pow",_) $ vv $ Free (d, _))) v =
5.17 + (Const ("Groups.times_class.times", _) $ t1 $ (Const ("Transcendental.powr",_) $ vv $ Free (d, _))) v =
5.18 if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME (TermC.int_of_str d) else NONE
5.19 - | factor_right_deg (Const ("Prog_Expr.pow",_) $ vv $ Free (d,_)) v =
5.20 + | factor_right_deg (Const ("Transcendental.powr",_) $ vv $ Free (d,_)) v =
5.21 if (vv = v) then SOME (TermC.int_of_str d) else NONE
5.22 | factor_right_deg (Const ("Groups.times_class.times",_) $ t1 $ vv) v =
5.23 if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME 1 else NONE
5.24 @@ -266,15 +266,15 @@
5.25 | monom2list t = [t];
5.26
5.27 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
5.28 -fun get_basStr (Const ("Prog_Expr.pow",_) $ Free (str, _) $ _) = str
5.29 +fun get_basStr (Const ("Transcendental.powr",_) $ Free (str, _) $ _) = str
5.30 | get_basStr (Free (str, _)) = str
5.31 | get_basStr _ = "|||"; (* gross gewichtet; für Brüch ect. *)
5.32 (*| get_basStr t =
5.33 raise ERROR("get_basStr: called with t= "^(UnparseC.term t));*)
5.34
5.35 (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
5.36 -fun get_potStr (Const ("Prog_Expr.pow",_) $ Free _ $ Free (str, _)) = str
5.37 - | get_potStr (Const ("Prog_Expr.pow",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *)
5.38 +fun get_potStr (Const ("Transcendental.powr",_) $ Free _ $ Free (str, _)) = str
5.39 + | get_potStr (Const ("Transcendental.powr",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *)
5.40 | get_potStr (Free (_, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)
5.41 | get_potStr _ = "||||||"; (* gross gewichtet; für Brüch ect. *)
5.42 (*| get_potStr t =
5.43 @@ -330,11 +330,11 @@
5.44 counter (n, xs)
5.45 else
5.46 (case x of
5.47 - (Const ("Prog_Expr.pow", _) $ Free _ $ Free (str_h, T)) =>
5.48 + (Const ("Transcendental.powr", _) $ Free _ $ Free (str_h, T)) =>
5.49 if (is_nums (Free (str_h, T))) then
5.50 counter (n + (the (TermC.int_opt_of_string str_h)), xs)
5.51 else counter (n + 1000, xs) (*FIXME.MG?!*)
5.52 - | (Const ("Prog_Expr.pow", _) $ Free _ $ _ ) =>
5.53 + | (Const ("Transcendental.powr", _) $ Free _ $ _ ) =>
5.54 counter (n + 1000, xs) (*FIXME.MG?!*)
5.55 | (Free _) => counter (n + 1, xs)
5.56 (*| _ => raise ERROR("monom_degree: called with factor: "^(UnparseC.term x)))*)
5.57 @@ -460,7 +460,7 @@
5.58
5.59 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
5.60 (case a of
5.61 - "Prog_Expr.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest string*)
5.62 + "Transcendental.powr" => ((("|||||||||||||", 0), T), 0) (*WN greatest string*)
5.63 | _ => (((a, 0), T), 0))
5.64 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
5.65 | dest_hd' (Var v) = (v, 2)
5.66 @@ -469,7 +469,7 @@
5.67 | dest_hd' t = raise TERM ("dest_hd'", [t]);
5.68
5.69 fun size_of_term' (Const(str,_) $ t) =
5.70 - if "Prog_Expr.pow"= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)
5.71 + if "Transcendental.powr"= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)
5.72 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
5.73 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
5.74 | size_of_term' _ = 1;
5.75 @@ -539,14 +539,14 @@
5.76 | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
5.77 | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
5.78 | is_polyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
5.79 - | is_polyexp (Const ("Prog_Expr.pow",_) $ Free _ $ Free _) = true
5.80 + | is_polyexp (Const ("Transcendental.powr",_) $ Free _ $ Free _) = true
5.81 | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
5.82 ((is_polyexp t1) andalso (is_polyexp t2))
5.83 | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
5.84 ((is_polyexp t1) andalso (is_polyexp t2))
5.85 | is_polyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =
5.86 ((is_polyexp t1) andalso (is_polyexp t2))
5.87 - | is_polyexp (Const ("Prog_Expr.pow",_) $ t1 $ t2) =
5.88 + | is_polyexp (Const ("Transcendental.powr",_) $ t1 $ t2) =
5.89 ((is_polyexp t1) andalso (is_polyexp t2))
5.90 | is_polyexp _ = false;
5.91 \<close>
5.92 @@ -657,7 +657,7 @@
5.93 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
5.94 Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
5.95 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
5.96 - Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_")];
5.97 + Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_")];
5.98
5.99 val poly_crls = Rule_Set.append_rules "poly_crls" Atools_crls
5.100 [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
5.101 @@ -665,7 +665,7 @@
5.102 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
5.103 Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
5.104 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
5.105 - Rule.Eval ("Prog_Expr.pow" , (**)eval_binop "#power_")];
5.106 + Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_")];
5.107 \<close>
5.108 ML \<open>
5.109 val expand =
5.110 @@ -800,12 +800,12 @@
5.111 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
5.112 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
5.113 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
5.114 - ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
5.115 + ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))
5.116 ],
5.117 errpatts = [],
5.118 rules = [Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
5.119 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
5.120 - Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_")
5.121 + Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_")
5.122 ], scr = Rule.Empty_Prog};
5.123
5.124 val reduce_012_mult_ =
5.125 @@ -951,7 +951,7 @@
5.126 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
5.127 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
5.128 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
5.129 - ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
5.130 + ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))
5.131 ], errpatts = [],
5.132 rules = [Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
5.133 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
5.134 @@ -964,7 +964,7 @@
5.135 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
5.136 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
5.137 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
5.138 - Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_")
5.139 + Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_")
5.140 ], scr = Rule.Empty_Prog};
5.141 val reduce_012 =
5.142 Rule_Def.Repeat{id = "reduce_012", preconds = [],
5.143 @@ -1062,7 +1062,7 @@
5.144 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
5.145 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
5.146 ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
5.147 - ("POWER" , ("Prog_Expr.pow", (**)eval_binop "#power_"))],
5.148 + ("POWER" , ("Transcendental.powr", (**)eval_binop "#power_"))],
5.149 errpatts = [],
5.150 scr = Rule.Rfuns {init_state = init_state,
5.151 normal_form = normal_form,
5.152 @@ -1101,7 +1101,7 @@
5.153 calc = [("PLUS" ,("Groups.plus_class.plus", (**)eval_binop "#add_")),
5.154 ("TIMES" ,("Groups.times_class.times", (**)eval_binop "#mult_")),
5.155 ("DIVIDE",("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
5.156 - ("POWER" ,("Prog_Expr.pow" , (**)eval_binop "#power_"))],
5.157 + ("POWER" ,("Transcendental.powr" , (**)eval_binop "#power_"))],
5.158 errpatts = [],
5.159 scr = Rule.Rfuns {init_state = init_state,
5.160 normal_form = normal_form,
5.161 @@ -1199,7 +1199,7 @@
5.162 erls = Atools_erls, srls = Rule_Set.Empty,
5.163 calc = [(*("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
5.164 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
5.165 - ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))*)
5.166 + ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))*)
5.167 ], errpatts = [],
5.168 rules = [Rule.Thm ("real_plus_binom_times" ,ThmC.numerals_to_Free @{thm real_plus_binom_times}),
5.169 (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
5.170 @@ -1222,7 +1222,7 @@
5.171
5.172 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
5.173 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
5.174 - Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_"),
5.175 + Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_"),
5.176
5.177 Rule.Thm ("sym_realpow_twoI",
5.178 ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
5.179 @@ -1248,7 +1248,7 @@
5.180
5.181 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
5.182 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
5.183 - Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_"),
5.184 + Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_"),
5.185
5.186 Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),(*"1 * z = z"*)
5.187 Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),(*"0 * z = 0"*)
5.188 @@ -1301,7 +1301,7 @@
5.189 erls = Atools_erls, srls = Rule_Set.Empty,
5.190 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
5.191 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
5.192 - ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
5.193 + ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))
5.194 ], errpatts = [],
5.195 rules = [Rule.Thm ("real_plus_binom_pow2",
5.196 ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
5.197 @@ -1356,7 +1356,7 @@
5.198
5.199 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
5.200 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
5.201 - Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_"),
5.202 + Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_"),
5.203 (*Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
5.204 (*AC-rewriting*)
5.205 Rule.Thm ("real_mult_left_commute",
5.206 @@ -1391,7 +1391,7 @@
5.207
5.208 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
5.209 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
5.210 - Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_")
5.211 + Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_")
5.212 ],
5.213 scr = Rule.Prog (Program.prep_program @{thm expand_binoms_2.simps})
5.214 };
6.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Sun May 02 15:55:37 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Mon May 03 08:49:50 2021 +0200
6.3 @@ -419,7 +419,7 @@
6.4 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
6.5 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
6.6 Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_"),
6.7 - Rule.Eval ("Prog_Expr.pow" , (**)eval_binop "#power_"),
6.8 + Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_"),
6.9 Rule.Rls_ reduce_012
6.10 ],
6.11 scr = Rule.Empty_Prog
6.12 @@ -1163,7 +1163,7 @@
6.13 | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
6.14 | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
6.15
6.16 -fun size_of_term' x (Const ("Prog_Expr.pow",_) $ Free (var,_) $ Free (pot,_)) =
6.17 +fun size_of_term' x (Const ("Transcendental.powr",_) $ Free (var,_) $ Free (pot,_)) =
6.18 (case x of (*WN*)
6.19 (Free (xstr,_)) =>
6.20 (if xstr = var then 1000*(the (TermC.int_opt_of_string pot)) else 3)
7.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Sun May 02 15:55:37 2021 +0200
7.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Mon May 03 08:49:50 2021 +0200
7.3 @@ -126,11 +126,11 @@
7.4 Free (num, _) $ Free _) $ Free (id, _)) =
7.5 if TermC.is_num' num then id
7.6 else "|||||||||||||"
7.7 - | identifier (Const ("Prog_Expr.pow", _) $ Free (base, _) $ Free (_(*exp*), _)) =
7.8 + | identifier (Const ("Transcendental.powr", _) $ Free (base, _) $ Free (_(*exp*), _)) =
7.9 if TermC.is_num' base then "|||||||||||||" (* a^2 *)
7.10 else (*increase*) base
7.11 | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *)
7.12 - (Const ("Prog_Expr.pow", _) $
7.13 + (Const ("Transcendental.powr", _) $
7.14 Free (base, _) $ Free (_(*exp*), _))) =
7.15 if TermC.is_num' num andalso not (TermC.is_num' base) then (*increase*) base
7.16 else "|||||||||||||"
7.17 @@ -169,10 +169,10 @@
7.18 (Const ("Groups.times_class.times", _) $
7.19 Free (num, _) $ Free _) $ Free (id, _)) =
7.20 if TermC.is_num' num andalso not (TermC.is_num' id) then true else false
7.21 - | ist_monom (Const ("Prog_Expr.pow", _) $ Free _ $ Free _) =
7.22 + | ist_monom (Const ("Transcendental.powr", _) $ Free _ $ Free _) =
7.23 true (* a^2 *)
7.24 | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *)
7.25 - (Const ("Prog_Expr.pow", _) $
7.26 + (Const ("Transcendental.powr", _) $
7.27 Free _ $ Free _)) =
7.28 if TermC.is_num' num then true else false
7.29 | ist_monom _ = false;
8.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sun May 02 15:55:37 2021 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon May 03 08:49:50 2021 +0200
8.3 @@ -25,7 +25,7 @@
8.4 | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
8.5 | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
8.6 | is_ratpolyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
8.7 - | is_ratpolyexp (Const ("Prog_Expr.pow",_) $ Free _ $ Free _) = true
8.8 + | is_ratpolyexp (Const ("Transcendental.powr",_) $ Free _ $ Free _) = true
8.9 | is_ratpolyexp (Const ("Rings.divide_class.divide",_) $ Free _ $ Free _) = true
8.10 | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
8.11 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
8.12 @@ -33,7 +33,7 @@
8.13 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
8.14 | is_ratpolyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =
8.15 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
8.16 - | is_ratpolyexp (Const ("Prog_Expr.pow",_) $ t1 $ t2) =
8.17 + | is_ratpolyexp (Const ("Transcendental.powr",_) $ t1 $ t2) =
8.18 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
8.19 | is_ratpolyexp (Const ("Rings.divide_class.divide",_) $ t1 $ t2) =
8.20 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
8.21 @@ -127,7 +127,7 @@
8.22 if TermC.is_num' id
8.23 then (id |> TermC.int_opt_of_string |> the |> curry op * c, es) (*several numerals in one monom*)
8.24 else (c, list_update es (find_index (curry op = t) vs) 1)
8.25 - | monom_of_term vs (c, es) (Const ("Prog_Expr.pow", _) $ (t as Free _) $ Free (e, _)) =
8.26 + | monom_of_term vs (c, es) (Const ("Transcendental.powr", _) $ (t as Free _) $ Free (e, _)) =
8.27 (c, list_update es (find_index (curry op = t) vs) (the (TermC.int_opt_of_string e)))
8.28 | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
8.29 let val (c', es') = monom_of_term vs (c, es) m1
8.30 @@ -138,7 +138,7 @@
8.31 [monom_of_term vs (1, replicate (length vs) 0) t]
8.32 | monoms_of_term vs (t as Free _) =
8.33 [monom_of_term vs (1, replicate (length vs) 0) t]
8.34 - | monoms_of_term vs (t as Const ("Prog_Expr.pow", _) $ _ $ _) =
8.35 + | monoms_of_term vs (t as Const ("Transcendental.powr", _) $ _ $ _) =
8.36 [monom_of_term vs (1, replicate (length vs) 0) t]
8.37 | monoms_of_term vs (t as Const ("Groups.times_class.times", _) $ _ $ _) =
8.38 [monom_of_term vs (1, replicate (length vs) 0) t]
8.39 @@ -179,7 +179,7 @@
8.40 | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
8.41 | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
8.42 | term_of_es baseT expT (v :: vs) (e :: es) =
8.43 - Const ("Prog_Expr.pow", [baseT, expT] ---> baseT) $ v $ (Free (TermC.isastr_of_int e, expT))
8.44 + Const ("Transcendental.powr", [baseT, expT] ---> baseT) $ v $ (Free (TermC.isastr_of_int e, expT))
8.45 :: term_of_es baseT expT vs es
8.46 | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
8.47
8.48 @@ -516,7 +516,7 @@
8.49 [("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
8.50 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
8.51 ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
8.52 - ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))],
8.53 + ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))],
8.54 errpatts = [],
8.55 scr =
8.56 Rule.Rfuns {init_state = init_state thy Atools_erls ro,
8.57 @@ -583,7 +583,7 @@
8.58 calc = [("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
8.59 ("TIMES", ("Groups.times_class.times", (**)eval_binop "#mult_")),
8.60 ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
8.61 - ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))],
8.62 + ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))],
8.63 errpatts = [],
8.64 scr = Rule.Rfuns {init_state = init_state thy Atools_erls ro,
8.65 normal_form = add_fraction_p_ thy,
9.1 --- a/src/Tools/isac/Knowledge/Root.thy Sun May 02 15:55:37 2021 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Root.thy Mon May 03 08:49:50 2021 +0200
9.3 @@ -167,7 +167,7 @@
9.4 [Rule.Thm ("real_unari_minus",ThmC.numerals_to_Free @{thm real_unari_minus}),
9.5 Rule.Eval ("NthRoot.sqrt" , eval_sqrt "#sqrt_"),
9.6 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
9.7 - Rule.Eval ("Prog_Expr.pow" , (**)eval_binop "#power_"),
9.8 + Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_"),
9.9 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
9.10 Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
9.11 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
9.12 @@ -179,7 +179,7 @@
9.13 [Rule.Thm ("real_unari_minus",ThmC.numerals_to_Free @{thm real_unari_minus}),
9.14 Rule.Eval ("NthRoot.sqrt" , eval_sqrt "#sqrt_"),
9.15 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
9.16 - Rule.Eval ("Prog_Expr.pow" , (**)eval_binop "#power_"),
9.17 + Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_"),
9.18 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
9.19 Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
9.20 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
9.21 @@ -249,7 +249,7 @@
9.22
9.23 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
9.24 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
9.25 - Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_")
9.26 + Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_")
9.27 ],
9.28 scr = Rule.Empty_Prog
9.29 });
9.30 @@ -298,7 +298,7 @@
9.31 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
9.32 Rule.Eval ("Rings.divide_class.divide" , Prog_Expr.eval_cancel "#divide_e"),
9.33 Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_"),
9.34 - Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_"),
9.35 + Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_"),
9.36
9.37 Rule.Thm ("sym_realpow_twoI",
9.38 ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
9.39 @@ -323,7 +323,7 @@
9.40 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
9.41 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
9.42 Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_"),
9.43 - Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_")
9.44 + Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_")
9.45 ],
9.46 scr = Rule.Empty_Prog
9.47 });
10.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Sun May 02 15:55:37 2021 +0200
10.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Mon May 03 08:49:50 2021 +0200
10.3 @@ -416,7 +416,7 @@
10.4 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
10.5 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
10.6 Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_"),
10.7 - Rule.Eval ("Prog_Expr.pow" , (**)eval_binop "#power_"),
10.8 + Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_"),
10.9 Rule.Thm("real_plus_binom_pow2",ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
10.10 Rule.Thm("real_minus_binom_pow2",ThmC.numerals_to_Free @{thm real_minus_binom_pow2}),
10.11 Rule.Thm("realpow_mul",ThmC.numerals_to_Free @{thm realpow_mul}),
11.1 --- a/src/Tools/isac/Knowledge/Test.thy Sun May 02 15:55:37 2021 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Test.thy Mon May 03 08:49:50 2021 +0200
11.3 @@ -295,7 +295,7 @@
11.4
11.5 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
11.6 (case a of
11.7 - "Prog_Expr.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest *)
11.8 + "Transcendental.powr" => ((("|||||||||||||", 0), T), 0) (*WN greatest *)
11.9 | _ => (((a, 0), T), 0))
11.10 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
11.11 | dest_hd' (Var v) = (v, 2)
11.12 @@ -312,7 +312,7 @@
11.13 \<close>
11.14
11.15 fun size_of_term' (Const(str,_) $ t) =
11.16 - if "Prog_Expr.pow"=str then 1000 + size_of_term' t else 1 + size_of_term' t(*WN*)
11.17 + if "Transcendental.powr"=str then 1000 + size_of_term' t else 1 + size_of_term' t(*WN*)
11.18 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
11.19 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
11.20 | size_of_term' _ = 1;
11.21 @@ -382,7 +382,7 @@
11.22
11.23 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
11.24 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
11.25 - Rule.Eval ("Prog_Expr.pow" , (**)eval_binop "#power_"),
11.26 + Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_"),
11.27
11.28 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
11.29 Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
11.30 @@ -427,7 +427,7 @@
11.31 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
11.32 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
11.33 Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_"),
11.34 - Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_"),
11.35 + Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_"),
11.36
11.37 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
11.38 Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
11.39 @@ -501,7 +501,7 @@
11.40 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
11.41 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
11.42 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
11.43 - Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_"),
11.44 + Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_"),
11.45
11.46 Rule.Thm ("rcollect_right",ThmC.numerals_to_Free @{thm rcollect_right}),
11.47 Rule.Thm ("rcollect_one_left",ThmC.numerals_to_Free @{thm rcollect_one_left}),
11.48 @@ -607,7 +607,7 @@
11.49 erls = testerls, srls = Rule_Set.Empty,
11.50 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
11.51 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
11.52 - ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
11.53 + ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))
11.54 ], errpatts = [],
11.55 rules = [Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
11.56 (*"a - b = a + (-1) * b"*)
11.57 @@ -663,7 +663,7 @@
11.58
11.59 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
11.60 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
11.61 - Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_")
11.62 + Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_")
11.63 ],
11.64 scr = Rule.Empty_Prog(*Rule.Prog ((Thm.term_of o the o (parse thy))
11.65 scr_make_polytest)*)
11.66 @@ -675,7 +675,7 @@
11.67 erls = testerls, srls = Rule_Set.Empty,
11.68 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
11.69 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
11.70 - ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
11.71 + ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))
11.72 ], errpatts = [],
11.73 rules =
11.74 [Rule.Thm ("real_plus_binom_pow2" ,ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
11.75 @@ -726,7 +726,7 @@
11.76
11.77 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
11.78 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
11.79 - Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_"),
11.80 + Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_"),
11.81 (*
11.82 Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
11.83 (*AC-rewriting*)
11.84 @@ -759,7 +759,7 @@
11.85
11.86 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
11.87 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
11.88 - Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_")
11.89 + Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_")
11.90 ],
11.91 scr = Rule.Empty_Prog
11.92 (*Program ((Thm.term_of o the o (parse thy)) scr_expand_binomtest)*)
12.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Sun May 02 15:55:37 2021 +0200
12.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Mon May 03 08:49:50 2021 +0200
12.3 @@ -15,8 +15,8 @@
12.4 \<close>
12.5
12.6 subsection \<open>Power re-defined for a specific type\<close>
12.7 -consts
12.8 - pow :: "[real, real] => real" (infixr "\<up>" 80)
12.9 +abbreviation real_powr :: "real \<Rightarrow> real \<Rightarrow> real" (infixr "\<up>" 80)
12.10 +where "x \<up> a \<equiv> x powr a"
12.11
12.12 subsection \<open>consts of functions in pre-conditions and program-expressions\<close>
12.13 consts
12.14 @@ -322,7 +322,7 @@
12.15 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
12.16 (*("PLUS" ,("Groups.plus_class.plus" , (**)eval_binop "#add_")),
12.17 ("TIMES" ,("Groups.times_class.times" , (**)eval_binop "#mult_")),
12.18 - ("POWER" ,("Prog_Expr.pow" , (**)eval_binop "#power_"))*)
12.19 + ("POWER" ,("Transcendental.powr" , (**)eval_binop "#power_"))*)
12.20
12.21 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
12.22 ("xxxxxx",op_,t,thy);
12.23 @@ -547,4 +547,4 @@
12.24 \<close> ML \<open>
12.25 \<close>
12.26
12.27 -end
12.28 \ No newline at end of file
12.29 +end
13.1 --- a/src/Tools/isac/ProgLang/evaluate.sml Sun May 02 15:55:37 2021 +0200
13.2 +++ b/src/Tools/isac/ProgLang/evaluate.sml Mon May 03 08:49:50 2021 +0200
13.3 @@ -225,7 +225,7 @@
13.4 ((a * c, b + d), (0, 0))
13.5 | calcul "Rings.divide_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
13.6 ((a div c, 0), (0, 0))
13.7 - | calcul "Prog_Expr.pow" ((a, _), _) ((c, _), _) = (*FIXXXME Float + prec.*)
13.8 + | calcul "Transcendental.powr" ((a, _), _) ((c, _), _) = (*FIXXXME Float + prec.*)
13.9 ((power a c, 0), (0, 0))
13.10 | calcul op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) =
13.11 raise ERROR ("calcul: not impl. for Float (("^
14.1 --- a/test/Tools/isac/Knowledge/integrate.sml Sun May 02 15:55:37 2021 +0200
14.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Mon May 03 08:49:50 2021 +0200
14.3 @@ -55,7 +55,7 @@
14.4 val t = str2t "Integral x \<up> 2 D x";
14.5 case t of
14.6 Const ("Integrate.Integral", _) $
14.7 - (Const ("Prog_Expr.pow", _) $ Free _ $ Free _) $ Free ("x", _) => ()
14.8 + (Const ("Transcendental.powr", _) $ Free _ $ Free _) $ Free ("x", _) => ()
14.9 | _ => error "integrate.sml: parsing: Integral x \<up> 2 D x";
14.10
14.11 val t = str2t "ff x is_f_x";
15.1 --- a/test/Tools/isac/Knowledge/rootrat.sml Sun May 02 15:55:37 2021 +0200
15.2 +++ b/test/Tools/isac/Knowledge/rootrat.sml Mon May 03 08:49:50 2021 +0200
15.3 @@ -36,7 +36,7 @@
15.4 [ Eval ("Groups.plus_class.plus",eval_binop "#add_"),
15.5 Eval ("Groups.minus_class.minus",eval_binop "#sub_"),
15.6 Eval ("Groups.times_class.times",eval_binop "#mult_"),
15.7 - Eval ("Prog_Expr.pow" ,eval_binop "#power_")
15.8 + Eval ("Transcendental.powr" ,eval_binop "#power_")
15.9 ];
15.10 val rls = calculate_Poly;
15.11
16.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Sun May 02 15:55:37 2021 +0200
16.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Mon May 03 08:49:50 2021 +0200
16.3 @@ -606,7 +606,7 @@
16.4 (*+*) Thm ("not_true", "(\<not> True) = False"),
16.5 (*+*) Thm ("not_false", "(\<not> False) = True"),
16.6 (*+*) :
16.7 -(*+*) Eval ("Prog_Expr.pow", fn),
16.8 +(*+*) Eval ("Transcendental.powr", fn),
16.9 (*+*) Eval ("RatEq.is'_ratequation'_in", fn)]:
16.10 (*+*) rule list*)
16.11 (*+*)chk: term list -> term list -> term list * bool
17.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Sun May 02 15:55:37 2021 +0200
17.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Mon May 03 08:49:50 2021 +0200
17.3 @@ -320,7 +320,7 @@
17.4 (filter Auto_Prog.is_calc) o Auto_Prog.stacpbls) sc;
17.5 case calcs of
17.6 [("PLUS", ("Groups.plus_class.plus", _)), ("TIMES", ("Groups.times_class.times", _)),
17.7 - ("DIVIDE", ("Rings.divide_class.divide", _)), ("POWER", ("Prog_Expr.pow", _))] => ()
17.8 + ("DIVIDE", ("Rings.divide_class.divide", _)), ("POWER", ("Transcendental.powr", _))] => ()
17.9 | _ => error "get_calcs changed"
17.10
17.11
18.1 --- a/test/Tools/isac/ProgLang/calculate.thy Sun May 02 15:55:37 2021 +0200
18.2 +++ b/test/Tools/isac/ProgLang/calculate.thy Mon May 03 08:49:50 2021 +0200
18.3 @@ -41,7 +41,7 @@
18.4 calc=[("PLUS", ("op +", eval_binop "#add_")),
18.5 ("TIMES", ("Groups.times_class.times", eval_binop "#mult_")),
18.6 ("DIVIDE", ("HOL.divide", Prog_Expr.eval_cancel "#divide_")),
18.7 - ("POWER", ("Prog_Expr.pow", eval_binop "#power_"))],
18.8 + ("POWER", ("Transcendental.powr", eval_binop "#power_"))],
18.9 crls=tval_rls, errpats = [], nrls= Rule_Set.empty (*, asm_rls=[],asm_thm=[]*)},
18.10 @{thm calc_test.simps})]
18.11 \<close>
19.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Sun May 02 15:55:37 2021 +0200
19.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Mon May 03 08:49:50 2021 +0200
19.3 @@ -48,7 +48,7 @@
19.4 val times = ("Groups.times_class.times", eval_binop "#mult_") : string * Eval_Def.eval_fn;
19.5 val plus = ("Groups.plus_class.plus",eval_binop "#add_") : string * Eval_Def.eval_fn;
19.6 val divide = ("Rings.divide_class.divide" ,eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
19.7 -val pow = ("Prog_Expr.pow" ,eval_binop "#power_") : string * Eval_Def.eval_fn;
19.8 +val pow = ("Transcendental.powr" ,eval_binop "#power_") : string * Eval_Def.eval_fn;
19.9
19.10 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, plus, t);
19.11 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
19.12 @@ -282,7 +282,7 @@
19.13
19.14 val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"));
19.15 (*
19.16 -val op_ = "Prog_Expr.pow" : string
19.17 +val op_ = "Transcendental.powr" : string
19.18 val eval_fn = fn : string -> term -> theory -> (string * term) option*)
19.19
19.20 val SOME (thmid,t') = get_pair thy op_ eval_fn t;