1.1 --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy	Thu Sep 16 12:23:57 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy	Thu Sep 16 17:23:54 2021 +0200
     1.3 @@ -6,6 +6,49 @@
     1.4  *)
     1.5  theory BaseDefinitions imports Know_Store
     1.6  begin
     1.7 +
     1.8 +subsection \<open>Power re-defined for a specific type\<close>
     1.9 +
    1.10 +definition even_real :: "real \<Rightarrow> bool"
    1.11 +  where "even_real x \<longleftrightarrow> \<bar>x\<bar> \<in> \<nat> \<and> even (inv real \<bar>x\<bar>)"
    1.12 +definition odd_real :: "real \<Rightarrow> bool"
    1.13 +  where "odd_real x \<longleftrightarrow> \<bar>x\<bar> \<in> \<nat> \<and> odd (inv real \<bar>x\<bar>)"
    1.14 +
    1.15 +definition realpow :: "real \<Rightarrow> real \<Rightarrow> real"  (infixr "\<up>" 80)
    1.16 +  where "x \<up> n =
    1.17 +    (if x \<ge> 0 then x powr n
    1.18 +     else if n \<ge> 0 \<and> even_real n then (- x) powr n
    1.19 +     else if n \<ge> 0 \<and> odd_real n then - ((- x) powr n)
    1.20 +     else if n < 0 \<and> even_real n then 1 / (- x) powr (- n)
    1.21 +     else if n < 0 \<and> odd_real n then - 1 / ((- x) powr (- n))
    1.22 +     else undefined)"
    1.23 +
    1.24 +lemma realpow_simps [simp]:
    1.25 +  "0 \<up> a = 0"
    1.26 +  "1 \<up> a = 1"
    1.27 +  "numeral m \<up> numeral n = (numeral m ^ numeral n :: real)"
    1.28 +  "x > 0 \<Longrightarrow> x \<up> 0 = 1"
    1.29 +  "x \<ge> 0 \<Longrightarrow> x \<up> 1 = x"
    1.30 +  "x \<ge> 0 \<Longrightarrow> x \<up> numeral n = x ^ numeral n"
    1.31 +  "x > 0 \<Longrightarrow> x \<up> - numeral n = 1 / (x ^ numeral n)"
    1.32 +  by (simp_all add: realpow_def powr_neg_numeral)
    1.33 +
    1.34 +lemma inv_real_eq:
    1.35 +  "inv real 0 = 0"
    1.36 +  "inv real 1 = 1"
    1.37 +  "inv real (numeral n) = numeral n"
    1.38 +  by (simp_all add: inv_f_eq)
    1.39 +
    1.40 +lemma realpow_uminus_simps [simp]:
    1.41 +  "(- numeral m) \<up> 0 = 1"
    1.42 +  "(- numeral m) \<up> 1 = - numeral m"
    1.43 +  "even (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (numeral n) = numeral m ^ numeral n"
    1.44 +  "odd (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (numeral n) = - (numeral m ^ numeral n)"
    1.45 +  "even (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (- numeral n) = 1 / (numeral m ^ numeral n)"
    1.46 +  "odd (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (- numeral n) = - 1 / (numeral m ^ numeral n)"
    1.47 +  by (simp_all add: realpow_def even_real_def odd_real_def inv_real_eq)
    1.48 +
    1.49 +
    1.50    ML_file termC.sml
    1.51    ML_file substitution.sml
    1.52    ML_file contextC.sml

     2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Thu Sep 16 12:23:57 2021 +0200
     2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Thu Sep 16 17:23:54 2021 +0200
     2.3 @@ -629,7 +629,7 @@
     2.4  val poly_consts = (* TODO: adopt syntax-const from Isabelle*)
     2.5    [\<^const_name>\<open>plus\<close>, \<^const_name>\<open>minus\<close>,
     2.6    \<^const_name>\<open>divide\<close>, \<^const_name>\<open>times\<close>,
     2.7 -  \<^const_name>\<open>powr\<close>];
     2.8 +  \<^const_name>\<open>realpow\<close>];
     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	Thu Sep 16 12:23:57 2021 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Thu Sep 16 17:23:54 2021 +0200
     3.3 @@ -37,7 +37,7 @@
     3.4  calculation MINUS (minus) = \<open>(**)eval_binop "#sub_"\<close>
     3.5  calculation TIMES (times) = \<open>(**)eval_binop "#mult_"\<close>
     3.6  calculation DIVIDE (divide) = \<open>Prog_Expr.eval_cancel "#divide_e"\<close>
     3.7 -calculation POWER (powr) = \<open>(**)eval_binop "#power_"\<close>
     3.8 +calculation POWER (realpow) = \<open>(**)eval_binop "#power_"\<close>
     3.9  calculation boollist2sum = \<open>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	Thu Sep 16 12:23:57 2021 +0200
     4.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Thu Sep 16 17:23:54 2021 +0200
     4.3 @@ -46,7 +46,7 @@
     4.4      (*		
     4.5       Don't use
     4.6       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
     4.7 -     \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
     4.8 +     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
     4.9       *)
    4.10      ];
    4.11  
    4.12 @@ -57,7 +57,7 @@
    4.13      (*		
    4.14       Don't use
    4.15       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
    4.16 -     \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
    4.17 +     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
    4.18       *)
    4.19      ];
    4.20  \<close>
    4.21 @@ -79,7 +79,7 @@
    4.22         \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
    4.23         \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
    4.24         *)
    4.25 -      \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")],
    4.26 +      \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
    4.27      scr = Rule.Empty_Prog});
    4.28  \<close>
    4.29  rule_set_knowledge LinPoly_simplify = LinPoly_simplify

     5.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Thu Sep 16 12:23:57 2021 +0200
     5.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Thu Sep 16 17:23:54 2021 +0200
     5.3 @@ -183,7 +183,7 @@
     5.4  val poly_consts =
     5.5    [\<^const_name>\<open>plus\<close>, \<^const_name>\<open>minus\<close>,
     5.6    \<^const_name>\<open>divide\<close>, \<^const_name>\<open>times\<close>,
     5.7 -  \<^const_name>\<open>powr\<close>];
     5.8 +  \<^const_name>\<open>realpow\<close>];
     5.9  
    5.10  val int_ord_SAVE = int_ord;
    5.11  (*for tests on rewrite orders*)
    5.12 @@ -201,10 +201,10 @@
    5.13    if (2) then v is a factor on the very right, casually with exponent.*)
    5.14  fun factor_right_deg (*case 2*)
    5.15  	    (Const (\<^const_name>\<open>Groups.times_class.times\<close>, _) $
    5.16 -        t1 $ (Const (\<^const_name>\<open>Transcendental.powr\<close>,_) $ vv $ num)) v =
    5.17 +        t1 $ (Const (\<^const_name>\<open>realpow\<close>,_) $ vv $ num)) v =
    5.18  	  if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME (snd (HOLogic.dest_number num))
    5.19      else NONE
    5.20 -  | factor_right_deg (Const (\<^const_name>\<open>Transcendental.powr\<close>,_) $ vv $ num) v =
    5.21 +  | factor_right_deg (Const (\<^const_name>\<open>realpow\<close>,_) $ vv $ num) v =
    5.22  	   if (vv = v) then SOME (snd (HOLogic.dest_number num)) else NONE
    5.23  
    5.24    | factor_right_deg (Const (\<^const_name>\<open>times\<close>,_) $ t1 $ vv) v = 
    5.25 @@ -279,16 +279,16 @@
    5.26    | monom2list t = [t];
    5.27  
    5.28  (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
    5.29 -fun get_basStr (Const (\<^const_name>\<open>powr\<close>,_) $ Free (str, _) $ _) = str
    5.30 -  | get_basStr (Const (\<^const_name>\<open>Transcendental.powr\<close>,_) $ n $ _) = TermC.to_string n
    5.31 +fun get_basStr (Const (\<^const_name>\<open>realpow\<close>,_) $ Free (str, _) $ _) = str
    5.32 +  | get_basStr (Const (\<^const_name>\<open>realpow\<close>,_) $ n $ _) = TermC.to_string n
    5.33    | get_basStr (Free (str, _)) = str
    5.34    | get_basStr t =
    5.35      if TermC.is_num t then TermC.to_string t
    5.36      else "|||"; (* gross gewichtet; für Brüche ect. *)
    5.37  
    5.38  (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
    5.39 -fun get_potStr (Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ Free _ $ Free (str, _)) = str
    5.40 -  | get_potStr (Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ Free _ $ t) =
    5.41 +fun get_potStr (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ Free (str, _)) = str
    5.42 +  | get_potStr (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =
    5.43      if TermC.is_num t then TermC.to_string t else "|||"
    5.44    | get_potStr (Free _) = "---" (* keine Hochzahl --> kleinst gewichtet *)
    5.45    | get_potStr _ = "||||||"; (* gross gewichtet; für Brüch ect. *)
    5.46 @@ -355,7 +355,7 @@
    5.47  	    if (is_nums x) then counter (n, xs)
    5.48  	    else 
    5.49  	      (case x of 
    5.50 -		      (Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ Free _ $ t) =>
    5.51 +		      (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =>
    5.52              if TermC.is_num t
    5.53              then counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs)
    5.54              else counter (n + 1000, xs) (*FIXME.MG?!*)
    5.55 @@ -500,7 +500,7 @@
    5.56  
    5.57  fun dest_hd' (Const (a, T)) =                          (* ~ term.ML *)
    5.58    (case a of
    5.59 -     \<^const_name>\<open>powr\<close> => ((("|||||||||||||", 0), T), 0)    (*WN greatest string*)
    5.60 +     \<^const_name>\<open>realpow\<close> => ((("|||||||||||||", 0), T), 0)    (*WN greatest string*)
    5.61     | _ => (((a, 0), T), 0))
    5.62    | dest_hd' (Free (a, T)) = (((a, 0), T), 1)(*TODOO handle this as numeral, too? see EqSystem.thy*)
    5.63    | dest_hd' (Var v) = (v, 2)
    5.64 @@ -509,7 +509,7 @@
    5.65    | dest_hd' t = raise TERM ("dest_hd'", [t]);
    5.66  
    5.67  fun size_of_term' (Const(str,_) $ t) =
    5.68 -  if \<^const_name>\<open>powr\<close>= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)
    5.69 +  if \<^const_name>\<open>realpow\<close>= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)
    5.70    | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
    5.71    | size_of_term' (f$t) = size_of_term' f  +  size_of_term' t
    5.72    | size_of_term' _ = 1;
    5.73 @@ -592,7 +592,7 @@
    5.74      if TermC.is_num num then true
    5.75      else if TermC.is_variable num then true
    5.76      else is_polyexp num
    5.77 -  | is_polyexp (Const (\<^const_name>\<open>Transcendental.powr\<close>,_) $ Free _ $ num) =
    5.78 +  | is_polyexp (Const (\<^const_name>\<open>realpow\<close>,_) $ Free _ $ num) =
    5.79      if TermC.is_num num then true
    5.80      else if TermC.is_variable num then true
    5.81      else is_polyexp num
    5.82 @@ -602,7 +602,7 @@
    5.83      ((is_polyexp t1) andalso (is_polyexp t2))
    5.84    | is_polyexp (Const (\<^const_name>\<open>Groups.times_class.times\<close>,_) $ t1 $ t2) = 
    5.85      ((is_polyexp t1) andalso (is_polyexp t2))
    5.86 -  | is_polyexp (Const (\<^const_name>\<open>Transcendental.powr\<close>,_) $ t1 $ t2) = 
    5.87 +  | is_polyexp (Const (\<^const_name>\<open>realpow\<close>,_) $ t1 $ t2) = 
    5.88      ((is_polyexp t1) andalso (is_polyexp t2))
    5.89    | is_polyexp num = TermC.is_num num;
    5.90  \<close>
    5.91 @@ -711,7 +711,7 @@
    5.92    \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
    5.93    \<^rule_eval>\<open>minus\<close> (eval_binop "#sub_"),
    5.94    \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
    5.95 -  \<^rule_eval>\<open>powr\<close> (eval_binop "#power_")];
    5.96 +  \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")];
    5.97  
    5.98  val poly_crls = Rule_Set.append_rules "poly_crls" Atools_crls [
    5.99    \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
   5.100 @@ -719,7 +719,7 @@
   5.101    \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
   5.102    \<^rule_eval>\<open>minus\<close> (eval_binop "#sub_"),
   5.103    \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
   5.104 -  \<^rule_eval>\<open>powr\<close> (eval_binop "#power_")];
   5.105 +  \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")];
   5.106  \<close>
   5.107  ML \<open>
   5.108  val expand =
   5.109 @@ -840,13 +840,13 @@
   5.110        erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
   5.111        calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), 
   5.112  	      ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
   5.113 -	      ("POWER", (\<^const_name>\<open>powr\<close>, eval_binop "#power_"))
   5.114 +	      ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))
   5.115  	      ],
   5.116        errpatts = [],
   5.117        rules = [
   5.118          \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
   5.119  	      \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
   5.120 -	      \<^rule_eval>\<open>powr\<close> (eval_binop "#power_")],
   5.121 +	      \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")],
   5.122        scr = Rule.Empty_Prog};
   5.123  
   5.124  val reduce_012_mult_ = 
   5.125 @@ -945,7 +945,7 @@
   5.126        erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
   5.127        calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), 
   5.128  	      ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
   5.129 -	      ("POWER", (\<^const_name>\<open>powr\<close>, eval_binop "#power_"))
   5.130 +	      ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))
   5.131  	      ], errpatts = [],
   5.132        rules =[
   5.133          \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
   5.134 @@ -955,7 +955,7 @@
   5.135  	      \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
   5.136  	      \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), 
   5.137  	      \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
   5.138 -	      \<^rule_eval>\<open>powr\<close> (eval_binop "#power_")],
   5.139 +	      \<^rule_eval>\<open>realpow\<close> (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 @@ -1035,7 +1035,7 @@
   5.144  	  calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
   5.145  		  ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
   5.146  		  ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
   5.147 -		  ("POWER" , (\<^const_name>\<open>powr\<close>, eval_binop "#power_"))],
   5.148 +		  ("POWER" , (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))],
   5.149      errpatts = [],
   5.150  	  scr = Rule.Rfuns {init_state  = init_state,
   5.151  		     normal_form = normal_form,
   5.152 @@ -1076,7 +1076,7 @@
   5.153        ("PLUS"  ,(\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
   5.154  		  ("TIMES" ,(\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
   5.155  		  ("DIVIDE",(\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
   5.156 -		  ("POWER" ,(\<^const_name>\<open>powr\<close>  , eval_binop "#power_"))],
   5.157 +		  ("POWER" ,(\<^const_name>\<open>realpow\<close>  , eval_binop "#power_"))],
   5.158  	  errpatts = [],
   5.159  	  scr = Rule.Rfuns {
   5.160        init_state  = init_state,
   5.161 @@ -1173,7 +1173,7 @@
   5.162      erls = Atools_erls, srls = Rule_Set.Empty,
   5.163      calc = [(*("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), 
   5.164  	    ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
   5.165 -	    ("POWER", (\<^const_name>\<open>powr\<close>, eval_binop "#power_"))*)
   5.166 +	    ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))*)
   5.167  	    ], errpatts = [],
   5.168      rules = [
   5.169         \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
   5.170 @@ -1191,7 +1191,7 @@
   5.171  
   5.172  	     \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), 
   5.173  	     \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
   5.174 -	     \<^rule_eval>\<open>powr\<close> (eval_binop "#power_"),
   5.175 +	     \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_"),
   5.176  	     
   5.177  	     \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
   5.178  	     \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)
   5.179 @@ -1206,7 +1206,7 @@
   5.180  
   5.181  	     \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
   5.182  	     \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
   5.183 -	     \<^rule_eval>\<open>powr\<close> (eval_binop "#power_"),
   5.184 +	     \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_"),
   5.185  
   5.186  	     \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
   5.187  	     \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
   5.188 @@ -1258,7 +1258,7 @@
   5.189      erls = Atools_erls, srls = Rule_Set.Empty,
   5.190      calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), 
   5.191  	    ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
   5.192 -	    ("POWER", (\<^const_name>\<open>powr\<close>, eval_binop "#power_"))
   5.193 +	    ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))
   5.194  	    ], errpatts = [],
   5.195      rules = [
   5.196         \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
   5.197 @@ -1287,7 +1287,7 @@
   5.198      
   5.199  	     \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), 
   5.200  	     \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
   5.201 -	     \<^rule_eval>\<open>powr\<close> (eval_binop "#power_"),
   5.202 +	     \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_"),
   5.203              (*\<^rule_thm>\<open>mult.commute\<close>,
   5.204  		    (*AC-rewriting*)
   5.205  	     \<^rule_thm>\<open>real_mult_left_commute\<close>,
   5.206 @@ -1309,7 +1309,7 @@
   5.207      
   5.208  	     \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), 
   5.209  	     \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
   5.210 -	     \<^rule_eval>\<open>powr\<close> (eval_binop "#power_")],
   5.211 +	     \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")],
   5.212      scr = Rule.Prog (Program.prep_program @{thm expand_binoms_2.simps})};      
   5.213  \<close>
   5.214  

     6.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Thu Sep 16 12:23:57 2021 +0200
     6.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Thu Sep 16 17:23:54 2021 +0200
     6.3 @@ -411,7 +411,7 @@
     6.4    		\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
     6.5    		\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
     6.6    		\<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
     6.7 -  		\<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
     6.8 +  		\<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
     6.9         Rule.Rls_ reduce_012],
    6.10      scr = Rule.Empty_Prog});
    6.11  \<close>
    6.12 @@ -1028,9 +1028,9 @@
    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' i pr x (t as Const (\<^const_name>\<open>powr\<close>, _) $ 
    6.17 +fun size_of_term' i pr x (t as Const (\<^const_name>\<open>realpow\<close>, _) $ 
    6.18        Free (var, _) $ Free (pot, _)) =
    6.19 -    (if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else ();
    6.20 +    (if pr then tracing (idt "#" i ^ "size_of_term' realpow: " ^ UnparseC.term t) else ();
    6.21      case x of                                                          (*WN*)
    6.22  	    (Free (xstr, _)) => 
    6.23  		    if xstr = var 

     7.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy	Thu Sep 16 12:23:57 2021 +0200
     7.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Thu Sep 16 17:23:54 2021 +0200
     7.3 @@ -124,13 +124,13 @@
     7.4            else "|||||||||||||"
     7.5        | _ => 
     7.6          (case t2 of
     7.7 -          Const (\<^const_name>\<open>powr\<close>, _) $ base $ exp => 
     7.8 +          Const (\<^const_name>\<open>realpow\<close>, _) $ base $ exp => 
     7.9              if TermC.is_atom base andalso TermC.is_atom exp then
    7.10                if TermC.is_num base then "|||||||||||||"
    7.11                else Free_to_string base
    7.12              else "|||||||||||||"
    7.13        | _ => "|||||||||||||"))
    7.14 -  | identifier (Const (\<^const_name>\<open>powr\<close>, _) $ base $ exp) =         (* _a_\<up>2, _3_^2          *)
    7.15 +  | identifier (Const (\<^const_name>\<open>realpow\<close>, _) $ base $ exp) =         (* _a_\<up>2, _3_^2          *)
    7.16      if TermC.is_atom base andalso TermC.is_atom exp then Free_to_string base
    7.17      else "|||||||||||||"
    7.18    | identifier t =                                                   (* 12                    *)
    7.19 @@ -165,7 +165,7 @@
    7.20      case t of
    7.21        Const (\<^const_name>\<open>Groups.times_class.times\<close>, _) $ t1 $ t2 =>
    7.22          ist_monom t1 andalso ist_monom t2
    7.23 -    | Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ t1 $ t2 =>
    7.24 +    | Const (\<^const_name>\<open>realpow\<close>, _) $ t1 $ t2 =>
    7.25          ist_monom t1 andalso ist_monom t2
    7.26      | _ => false
    7.27  

     8.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Thu Sep 16 12:23:57 2021 +0200
     8.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Thu Sep 16 17:23:54 2021 +0200
     8.3 @@ -25,7 +25,7 @@
     8.4    | is_ratpolyexp (Const (\<^const_name>\<open>plus\<close>,_) $ Free _ $ Free _) = true
     8.5    | is_ratpolyexp (Const (\<^const_name>\<open>minus\<close>,_) $ Free _ $ Free _) = true
     8.6    | is_ratpolyexp (Const (\<^const_name>\<open>times\<close>,_) $ Free _ $ Free _) = true
     8.7 -  | is_ratpolyexp (Const (\<^const_name>\<open>powr\<close>,_) $ Free _ $ Free _) = true
     8.8 +  | is_ratpolyexp (Const (\<^const_name>\<open>realpow\<close>,_) $ Free _ $ Free _) = true
     8.9    | is_ratpolyexp (Const (\<^const_name>\<open>divide\<close>,_) $ Free _ $ Free _) = true
    8.10    | is_ratpolyexp (Const (\<^const_name>\<open>plus\<close>,_) $ 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 (\<^const_name>\<open>times\<close>,_) $ t1 $ t2) = 
    8.15                 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
    8.16 -  | is_ratpolyexp (Const (\<^const_name>\<open>powr\<close>,_) $ t1 $ t2) = 
    8.17 +  | is_ratpolyexp (Const (\<^const_name>\<open>realpow\<close>,_) $ t1 $ t2) = 
    8.18                 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
    8.19    | is_ratpolyexp (Const (\<^const_name>\<open>divide\<close>,_) $ t1 $ t2) = 
    8.20                 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
    8.21 @@ -131,10 +131,10 @@
    8.22      (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
    8.23    | monom_of_term  vs (c, es) (t as Free _) =
    8.24      (c, list_update es (find_index (curry op = t) vs) 1)
    8.25 -  | monom_of_term  vs (c, es) (Const (\<^const_name>\<open>powr\<close>, _) $ (b as Free _) $
    8.26 +  | monom_of_term  vs (c, es) (Const (\<^const_name>\<open>realpow\<close>, _) $ (b as Free _) $
    8.27        (e as Const (\<^const_name>\<open>numeral\<close>, _) $ _)) =
    8.28      (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
    8.29 -  | monom_of_term  vs (c, es) (Const (\<^const_name>\<open>powr\<close>, _) $ (b as Free _) $
    8.30 +  | monom_of_term  vs (c, es) (Const (\<^const_name>\<open>realpow\<close>, _) $ (b as Free _) $
    8.31        (e as Const (\<^const_name>\<open>uminus\<close>, _) $ _)) =
    8.32      (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
    8.33  
    8.34 @@ -154,7 +154,7 @@
    8.35      [monom_of_term  vs (1, replicate (length vs) 0) t]
    8.36    | monoms_of_term vs (t as Free _) =
    8.37      [monom_of_term  vs (1, replicate (length vs) 0) t]
    8.38 -  | monoms_of_term vs (t as Const (\<^const_name>\<open>powr\<close>, _) $ _ $  _) =
    8.39 +  | monoms_of_term vs (t as Const (\<^const_name>\<open>realpow\<close>, _) $ _ $  _) =
    8.40      [monom_of_term  vs (1, replicate (length vs) 0) t]
    8.41    | monoms_of_term vs (t as Const (\<^const_name>\<open>times\<close>, _) $ _ $  _) =
    8.42      [monom_of_term  vs (1, replicate (length vs) 0) t]
    8.43 @@ -195,7 +195,7 @@
    8.44    | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
    8.45    | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
    8.46    | term_of_es baseT expT (v :: vs) (e :: es) =
    8.47 -    Const (\<^const_name>\<open>Transcendental.powr\<close>, [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
    8.48 +    Const (\<^const_name>\<open>realpow\<close>, [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
    8.49      :: term_of_es baseT expT vs es
    8.50    | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
    8.51  
    8.52 @@ -519,7 +519,7 @@
    8.53  	  [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
    8.54  	  ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
    8.55  	  ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
    8.56 -	  ("POWER", (\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_"))],
    8.57 +	  ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))],
    8.58      errpatts = [],
    8.59  	scr =
    8.60  	  Rule.Rfuns {init_state  = init_state \<^theory> Atools_erls ro,
    8.61 @@ -586,7 +586,7 @@
    8.62      calc = [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
    8.63        ("TIMES", (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
    8.64        ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
    8.65 -      ("POWER", (\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_"))],
    8.66 +      ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))],
    8.67      errpatts = [],
    8.68      scr = Rule.Rfuns {init_state  = init_state \<^theory> Atools_erls ro,
    8.69        normal_form = add_fraction_p_ \<^theory>,

     9.1 --- a/src/Tools/isac/Knowledge/Root.thy	Thu Sep 16 12:23:57 2021 +0200
     9.2 +++ b/src/Tools/isac/Knowledge/Root.thy	Thu Sep 16 17:23:54 2021 +0200
     9.3 @@ -161,7 +161,7 @@
     9.4      \<^rule_thm>\<open>real_unari_minus\<close>,
     9.5      \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
     9.6      \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
     9.7 -    \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
     9.8 +    \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
     9.9      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
    9.10      \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
    9.11      \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
    9.12 @@ -172,7 +172,7 @@
    9.13      \<^rule_thm>\<open>real_unari_minus\<close>,
    9.14      \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
    9.15      \<^rule_eval>\<open>Rings.divide_class.divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
    9.16 -    \<^rule_eval>\<open>Transcendental.powr\<close> (**)(eval_binop "#power_"),
    9.17 +    \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
    9.18      \<^rule_eval>\<open>Groups.plus_class.plus\<close> (**)(eval_binop "#add_"), 
    9.19      \<^rule_eval>\<open>Groups.minus_class.minus\<close> (**)(eval_binop "#sub_"),
    9.20      \<^rule_eval>\<open>Groups.times_class.times\<close> (**)(eval_binop "#mult_"),
    9.21 @@ -223,7 +223,7 @@
    9.22  
    9.23        \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
    9.24        \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
    9.25 -      \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")],
    9.26 +      \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
    9.27      scr = Rule.Empty_Prog});      
    9.28  \<close>
    9.29  rule_set_knowledge make_rooteq = make_rooteq
    9.30 @@ -258,7 +258,7 @@
    9.31         \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
    9.32         \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
    9.33         \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
    9.34 -       \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
    9.35 +       \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
    9.36    
    9.37         \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1  \<up>  2"*)
    9.38         \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r  \<up>  n = r  \<up>  (n + 1)"*)
    9.39 @@ -274,7 +274,7 @@
    9.40         \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
    9.41         \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
    9.42         \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
    9.43 -       \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")],
    9.44 +       \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
    9.45      scr = Rule.Empty_Prog});      
    9.46  \<close>
    9.47  rule_set_knowledge expand_rootbinoms = expand_rootbinoms

    10.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Thu Sep 16 12:23:57 2021 +0200
    10.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Thu Sep 16 17:23:54 2021 +0200
    10.3 @@ -323,7 +323,7 @@
    10.4        \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
    10.5        \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
    10.6        \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
    10.7 -      \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
    10.8 +      \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
    10.9        \<^rule_thm>\<open>real_plus_binom_pow2\<close>,
   10.10        \<^rule_thm>\<open>real_minus_binom_pow2\<close>,
   10.11        \<^rule_thm>\<open>realpow_mul\<close>, (* (a * b)^n = a^n * b^n*)

    11.1 --- a/src/Tools/isac/Knowledge/Test.thy	Thu Sep 16 12:23:57 2021 +0200
    11.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Thu Sep 16 17:23:54 2021 +0200
    11.3 @@ -292,7 +292,7 @@
    11.4  
    11.5  fun dest_hd' (Const (a, T)) =                          (* ~ term.ML *)
    11.6      (case a of
    11.7 -      \<^const_name>\<open>powr\<close> => ((("|||||||||||||", 0), T), 0)           (*WN greatest *)
    11.8 +      \<^const_name>\<open>realpow\<close> => ((("|||||||||||||", 0), T), 0)           (*WN greatest *)
    11.9    | _ => (((a, 0), T), 0))
   11.10    | dest_hd' (Free (a, T)) = (((a, 0), T), 1)(*TODOO handle this as numeral, too? see EqSystem.thy*)
   11.11    | dest_hd' (Var v) = (v, 2)
   11.12 @@ -309,7 +309,7 @@
   11.13  \<close>
   11.14  
   11.15  fun size_of_term' (Const(str,_) $ t) =
   11.16 -  if \<^const_name>\<open>powr\<close>=str then 1000 + size_of_term' t else 1 + size_of_term' t(*WN*)
   11.17 +  if \<^const_name>\<open>realpow\<close>=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 @@ -380,7 +380,7 @@
   11.22      
   11.23  	     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
   11.24  	     \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
   11.25 -	     \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
   11.26 +	     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
   11.27      
   11.28  	     \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
   11.29  	     \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
   11.30 @@ -424,7 +424,7 @@
   11.31  	     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
   11.32  	     \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
   11.33  	     \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
   11.34 -	     \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
   11.35 +	     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
   11.36      
   11.37  	     \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
   11.38  	     \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
   11.39 @@ -497,7 +497,7 @@
   11.40  	     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
   11.41  	     \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
   11.42  	     \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
   11.43 -	     \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
   11.44 +	     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
   11.45  
   11.46  	     \<^rule_thm>\<open>rcollect_right\<close>,
   11.47  	     \<^rule_thm>\<open>rcollect_one_left\<close>,
   11.48 @@ -602,7 +602,7 @@
   11.49      calc = [
   11.50        ("PLUS"  , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), 
   11.51  	    ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
   11.52 -	    ("POWER", (\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_"))],
   11.53 +	    ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))],
   11.54      errpatts = [],
   11.55      rules = [
   11.56         \<^rule_thm>\<open>real_diff_minus\<close>, (*"a - b = a + (-1) * b"*)
   11.57 @@ -633,7 +633,7 @@
   11.58      
   11.59  	     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
   11.60  	     \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
   11.61 -	     \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")],
   11.62 +	     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
   11.63      scr = Rule.Empty_Prog}; 
   11.64  
   11.65  val expand_binomtest =
   11.66 @@ -642,7 +642,7 @@
   11.67      calc = [
   11.68        ("PLUS"  , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), 
   11.69  	    ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
   11.70 -	    ("POWER", (\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_"))
   11.71 +	    ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))
   11.72  	    ],
   11.73      errpatts = [],
   11.74      rules = [
   11.75 @@ -667,7 +667,7 @@
   11.76      
   11.77      	\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
   11.78      	\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
   11.79 -    	\<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
   11.80 +    	\<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
   11.81      
   11.82      	\<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
   11.83      	\<^rule_thm>\<open>realpow_plus_1\<close>,	 (*"r * r \<up> n = r \<up> (n + 1)"*)
   11.84 @@ -681,7 +681,7 @@
   11.85      
   11.86      	\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
   11.87      	\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
   11.88 -    	\<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")],
   11.89 +    	\<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
   11.90      scr = Rule.Empty_Prog};      
   11.91  \<close>
   11.92  rule_set_knowledge

    12.1 --- a/src/Tools/isac/ProgLang/Calculate.thy	Thu Sep 16 12:23:57 2021 +0200
    12.2 +++ b/src/Tools/isac/ProgLang/Calculate.thy	Thu Sep 16 17:23:54 2021 +0200
    12.3 @@ -27,7 +27,7 @@
    12.4  val is_num = can HOLogic.dest_number;
    12.5  
    12.6  val is_calcul_op =
    12.7 -  member (op =) [\<^const_name>\<open>plus\<close>, \<^const_name>\<open>minus\<close>, \<^const_name>\<open>times\<close>, \<^const_name>\<open>powr\<close>];
    12.8 +  member (op =) [\<^const_name>\<open>plus\<close>, \<^const_name>\<open>minus\<close>, \<^const_name>\<open>times\<close>, \<^const_name>\<open>realpow\<close>];
    12.9  
   12.10  fun calcul thy lhs =
   12.11    let

    13.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Thu Sep 16 12:23:57 2021 +0200
    13.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Thu Sep 16 17:23:54 2021 +0200
    13.3 @@ -14,10 +14,6 @@
    13.4    (all named eval_*), such that Isac's rewrite engine can handle it.
    13.5  \<close>
    13.6  
    13.7 -subsection \<open>Power re-defined for a specific type\<close>
    13.8 -abbreviation real_powr :: "real \<Rightarrow> real \<Rightarrow> real"  (infixr "\<up>" 80)
    13.9 -where "x \<up> a \<equiv> x powr a"
   13.10 -
   13.11  subsection \<open>consts of functions in pre-conditions and program-expressions\<close>
   13.12  consts
   13.13    lhs             :: "bool => real"           (*of an equality*)
   13.14 @@ -307,7 +303,7 @@
   13.15  (*. evaluate binary, associative, commutative operators: *,+,^ .*)
   13.16  (*("PLUS"    ,(\<^const_name>\<open>plus\<close>        , (**)eval_binop "#add_")),
   13.17    ("TIMES"   ,(\<^const_name>\<open>times\<close>        , (**)eval_binop "#mult_")),
   13.18 -  ("POWER"  ,(\<^const_name>\<open>powr\<close>  , (**)eval_binop "#power_"))*)
   13.19 +  ("POWER"  ,(\<^const_name>\<open>realpow\<close>  , (**)eval_binop "#power_"))*)
   13.20  
   13.21  (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
   13.22         ("xxxxxx",op_,t,thy);

    14.1 --- a/test/Tools/isac/BaseDefinitions/kestore.sml	Thu Sep 16 12:23:57 2021 +0200
    14.2 +++ b/test/Tools/isac/BaseDefinitions/kestore.sml	Thu Sep 16 17:23:54 2021 +0200
    14.3 @@ -95,6 +95,6 @@
    14.4  (*+*)map (fst o snd) calcs = (*..WITH declare [[ML_print_depth = 999]]*)
    14.5     ["Test.precond_rootmet", "Test.contains_root", "Test.precond_rootpbl", "Integrate.is_f_x", "Diff.primed", "RootEq.is_normSqrtTerm_in", "RootEq.is_rootTerm_in", "NthRoot.sqrt", "RootEq.is_sqrtTerm_in",
    14.6      "RatEq.is_ratequation_in", "RootRatEq.is_rootRatAddTerm_in", "Integrate.add_new_c", "EqSystem.occur_exactly_in", "Poly.is_addUnordered", "Poly.is_polyexp", "Poly.is_poly_in", "Poly.is_polyrat_in",
    14.7 -    "Transcendental.powr", "Groups.times_class.times", "Groups.plus_class.plus", "Prog_Expr.ident", "Orderings.ord_class.less", "Prog_Expr.is_atom", "Prog_Expr.occurs_in", "Prog_Expr.is_num", "Prog_Expr.matchsub",
    14.8 +    \<^const_name>\<open>realpow\<close>, "Groups.times_class.times", "Groups.plus_class.plus", "Prog_Expr.ident", "Orderings.ord_class.less", "Prog_Expr.is_atom", "Prog_Expr.occurs_in", "Prog_Expr.is_num", "Prog_Expr.matchsub",
    14.9      "Prog_Expr.Vars", "Prog_Expr.lhs", "Prog_Expr.rhs", "Prog_Expr.matches", "Prog_Expr.some_occur_in", "Prog_Expr.is_even", "Orderings.ord_class.less_eq", "HOL.eq", "Groups.minus_class.minus",
   14.10      "Rings.divide_class.divide", "Prog_Expr.boollist2sum", "Poly.is_expanded_in", "Poly.has_degree_in", "Poly.is_multUnordered", "Rational.is_expanded"];

    15.1 --- a/test/Tools/isac/Knowledge/integrate.sml	Thu Sep 16 12:23:57 2021 +0200
    15.2 +++ b/test/Tools/isac/Knowledge/integrate.sml	Thu Sep 16 17:23:54 2021 +0200
    15.3 @@ -55,7 +55,7 @@
    15.4  val t = TermC.str2term "Integral x \<up> 2 D x";
    15.5  case t of 
    15.6      Const (\<^const_name>\<open>Integral\<close>, _) $
    15.7 -     (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ _) $ Free ("x", _) => ()
    15.8 +     (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ _) $ Free ("x", _) => ()
    15.9    | _ => error "integrate.sml: parsing: Integral x \<up> 2 D x";
   15.10  
   15.11  val t = TermC.str2term "ff x is_f_x";

    16.1 --- a/test/Tools/isac/Knowledge/poly-1.sml	Thu Sep 16 12:23:57 2021 +0200
    16.2 +++ b/test/Tools/isac/Knowledge/poly-1.sml	Thu Sep 16 17:23:54 2021 +0200
    16.3 @@ -362,7 +362,7 @@
    16.4  "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee1);
    16.5  "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
    16.6  	    (*if*) (is_nums x) (*else*);
    16.7 -  val (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ t) =
    16.8 +  val (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =
    16.9        (*case*) x (*of*); 
   16.10  (*+*)UnparseC.term x = "x \<up> 2";
   16.11              (*if*) TermC.is_num t (*then*);
   16.12 @@ -370,7 +370,7 @@
   16.13             counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
   16.14  "~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
   16.15  	    (*if*) (is_nums x) (*else*);
   16.16 -  val (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ t) =
   16.17 +  val (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =
   16.18        (*case*) x (*of*); 
   16.19  (*+*)UnparseC.term x = "y \<up> 2";
   16.20              (*if*) TermC.is_num t (*then*);
   16.21 @@ -385,7 +385,7 @@
   16.22  "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee2);
   16.23  "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
   16.24  	    (*if*) (is_nums x) (*else*);
   16.25 -val (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ t) =
   16.26 +val (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =
   16.27        (*case*) x (*of*); 
   16.28  (*+*)UnparseC.term x = "x \<up> 3";
   16.29              (*if*) TermC.is_num t (*then*);

    17.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Thu Sep 16 12:23:57 2021 +0200
    17.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Thu Sep 16 17:23:54 2021 +0200
    17.3 @@ -243,9 +243,9 @@
    17.4    | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
    17.5    | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
    17.6  
    17.7 -fun size_of_term' i pr x (t as Const (\<^const_name>\<open>powr\<close>, _) $ 
    17.8 +fun size_of_term' i pr x (t as Const (\<^const_name>\<open>realpow\<close>, _) $ 
    17.9        Free (var, _) $ Free (pot, _)) =
   17.10 -    (if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else ();
   17.11 +    (if pr then tracing (idt "#" i ^ "size_of_term' realpow: " ^ UnparseC.term t) else ();
   17.12      case x of                                                          (*WN*)
   17.13  	    (Free (xstr, _)) => 
   17.14  		    if xstr = var 

    18.1 --- a/test/Tools/isac/Knowledge/rational-1.sml	Thu Sep 16 12:23:57 2021 +0200
    18.2 +++ b/test/Tools/isac/Knowledge/rational-1.sml	Thu Sep 16 17:23:54 2021 +0200
    18.3 @@ -51,13 +51,13 @@
    18.4      val (c', es') =
    18.5  
    18.6             monom_of_term vs (c, es) m1;
    18.7 -"~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (\<^const_name>\<open>powr\<close>, _) $ (t as Free _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ num)) ) =
    18.8 +"~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (\<^const_name>\<open>realpow\<close>, _) $ (t as Free _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ num)) ) =
    18.9    (vs, (c', es'), m2);
   18.10  (*+*)c = 12;
   18.11  (*+*)(num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = [3, 0, 0];
   18.12  
   18.13  if (c, num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = (12, [3, 0, 0])
   18.14 -then () else error "monom_of_term (powr): return value CHANGED";
   18.15 +then () else error "monom_of_term (realpow): return value CHANGED";
   18.16  
   18.17  if poly_of_term vs (TermC.str2term "12 * x \<up> 3 * y \<up> 4 * z \<up> 6") = SOME [(12, [3, 4, 6])]
   18.18  then () else error "poly_of_term 4 changed";

    19.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Thu Sep 16 12:23:57 2021 +0200
    19.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Thu Sep 16 17:23:54 2021 +0200
    19.3 @@ -381,7 +381,7 @@
    19.4  (*+*)       (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
    19.5  (*+*)         (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $
    19.6  (*+*)           (Const (\<^const_name>\<open>times\<close>, _) $
    19.7 -(*+*)             (Const (\<^const_name>\<open>powr\<close>, _) $ Free ("x", _) $ _ ) $ Free ("x", _))) $
    19.8 +(*+*)             (Const (\<^const_name>\<open>realpow\<close>, _) $ Free ("x", _) $ _ ) $ Free ("x", _))) $
    19.9  (*+*)         Const (\<^const_name>\<open>True\<close>, _))) => ()
   19.10  (*+*)(*                   ^^^^^^             compare ---vvv *)
   19.11  (*+*)| _ => error "rewrite.sml diff. eval_is_multUnordered 2b CHANGED";
   19.12 @@ -622,7 +622,7 @@
   19.13  (*+*)    Thm ("not_true", "(\<not> True) = False"),
   19.14  (*+*)    Thm ("not_false", "(\<not> False) = True"),
   19.15  (*+*)    :
   19.16 -(*+*)    Eval (\<^const_name>\<open>powr\<close>, fn),
   19.17 +(*+*)    Eval (\<^const_name>\<open>realpow\<close>, fn),
   19.18  (*+*)    Eval ("RatEq.is_ratequation_in", fn)]:
   19.19  (*+*)   rule list*)
   19.20  (*+*)chk: term list -> term list -> term list * bool

    20.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml	Thu Sep 16 12:23:57 2021 +0200
    20.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml	Thu Sep 16 17:23:54 2021 +0200
    20.3 @@ -320,7 +320,7 @@
    20.4    (filter Auto_Prog.is_calc) o Auto_Prog.stacpbls) sc;
    20.5  case calcs of
    20.6    [("PLUS", (\<^const_name>\<open>plus\<close>, _)), ("TIMES", (\<^const_name>\<open>times\<close>, _)), 
    20.7 -  ("DIVIDE", (\<^const_name>\<open>divide\<close>, _)), ("POWER", (\<^const_name>\<open>powr\<close>, _))] => ()
    20.8 +  ("DIVIDE", (\<^const_name>\<open>divide\<close>, _)), ("POWER", (\<^const_name>\<open>realpow\<close>, _))] => ()
    20.9  | _ => error "get_calcs changed"
   20.10  
   20.11  

    21.1 --- a/test/Tools/isac/ProgLang/calculate.sml	Thu Sep 16 12:23:57 2021 +0200
    21.2 +++ b/test/Tools/isac/ProgLang/calculate.sml	Thu Sep 16 17:23:54 2021 +0200
    21.3 @@ -20,7 +20,7 @@
    21.4  test \<^theory> \<^term>\<open>10 + 20 :: real\<close>;
    21.5  test \<^theory> \<^term>\<open>10 - 20 :: real\<close>;
    21.6  test \<^theory> \<^term>\<open>10 * 20 :: real\<close>;
    21.7 -test \<^theory> \<^term>\<open>10 powr 20 :: real\<close>;
    21.8 +test \<^theory> \<^term>\<open>10 \<up> 20 :: real\<close>;
    21.9  
   21.10  test \<^theory> \<^term>\<open>10 + 20 :: int\<close>;
   21.11  test \<^theory> \<^term>\<open>10 - 20 :: int\<close>;

    22.1 --- a/test/Tools/isac/ProgLang/calculate.thy	Thu Sep 16 12:23:57 2021 +0200
    22.2 +++ b/test/Tools/isac/ProgLang/calculate.thy	Thu Sep 16 17:23:54 2021 +0200
    22.3 @@ -41,7 +41,7 @@
    22.4            calc=[("PLUS", (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
    22.5                ("TIMES", (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
    22.6                ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_")),
    22.7 -              ("POWER", (\<^const_name>\<open>powr\<close>, eval_binop "#power_"))],
    22.8 +              ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))],
    22.9            crls=tval_rls, errpats = [], nrls= Rule_Set.empty (*, asm_rls=[],asm_thm=[]*)},
   22.10          @{thm calc_test.simps})]
   22.11  \<close>

    23.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Thu Sep 16 12:23:57 2021 +0200
    23.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Thu Sep 16 17:23:54 2021 +0200
    23.3 @@ -51,7 +51,7 @@
    23.4  val times =  ("Groups.times_class.times", eval_binop "#mult_") : string * Eval_Def.eval_fn;
    23.5  val plus =   ("Groups.plus_class.plus", eval_binop "#add_") : string * Eval_Def.eval_fn;
    23.6  val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
    23.7 -val pow =    ("Transcendental.powr", eval_binop "#power_") : string * Eval_Def.eval_fn;
    23.8 +val pow =    (\<^const_name>\<open>realpow\<close>, eval_binop "#power_") : string * Eval_Def.eval_fn;
    23.9  
   23.10  "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
   23.11  val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
   23.12 @@ -269,7 +269,7 @@
   23.13  
   23.14    val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"));
   23.15    (*
   23.16 -val op_ = \<^const_name>\<open>powr\<close> : string
   23.17 +val op_ = \<^const_name>\<open>realpow\<close> : string
   23.18  val eval_fn = fn : string -> term -> theory -> (string * term) option*)
   23.19  
   23.20    val SOME (thmid,t') = get_pair thy op_ eval_fn t;
   23.21 @@ -279,8 +279,8 @@
   23.22  (*** calc: operator = pow not defined*)
   23.23  
   23.24  case (op_, t) of
   23.25 -  ("Transcendental.powr",
   23.26 -    Const (\<^const_name>\<open>powr\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $
   23.27 +  (\<^const_name>\<open>realpow\<close>,
   23.28 +    Const (\<^const_name>\<open>realpow\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $
   23.29        (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()
   23.30  | _ => error "3 \<up> 2 CHANGED";
   23.31    val SOME (id, t') = eval_binop thmid op_ t thy;

    24.1 --- a/test/Tools/isac/Test_Some.thy	Thu Sep 16 12:23:57 2021 +0200
    24.2 +++ b/test/Tools/isac/Test_Some.thy	Thu Sep 16 17:23:54 2021 +0200
    24.3 @@ -358,9 +358,9 @@
    24.4    | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
    24.5    | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
    24.6  
    24.7 -fun size_of_term' i pr x (t as Const (\<^const_name>\<open>powr\<close>, _) $ 
    24.8 +fun size_of_term' i pr x (t as Const (\<^const_name>\<open>realpow\<close>, _) $ 
    24.9        Free (var, _) $ Free (pot, _)) =
   24.10 -    (if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else ();
   24.11 +    (if pr then tracing (idt "#" i ^ "size_of_term' realpow: " ^ UnparseC.term t) else ();
   24.12      case x of                                                          (*WN*)
   24.13  	    (Free (xstr, _)) => 
   24.14  		    if xstr = var