1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Wed Aug 18 11:35:24 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Wed Aug 18 16:03:08 2021 +0200
     1.3 @@ -41,7 +41,6 @@
     1.4  
     1.5    val is_atom: term -> bool
     1.6    val string_of_atom: term -> string
     1.7 -  val is_const: term -> bool
     1.8    val is_variable: term -> bool
     1.9    val is_bdv: string -> bool
    1.10    val is_bdv_subst: term -> bool
    1.11 @@ -290,7 +289,6 @@
    1.12  (* accomodate string-representation for int to term-orders *)
    1.13  fun to_string t = t |> num_of_term |> signed_string_of_int
    1.14  
    1.15 -fun is_const (Const _) = true | is_const _ = false;
    1.16  fun is_variable (t as Free _) = not (is_num t)
    1.17    | is_variable _ = false;
    1.18  fun is_Free (Free _) = true | is_Free _ = false;
    1.19 @@ -300,6 +298,7 @@
    1.20  fun is_f_x (f $ x) = is_fun_id f andalso is_Free x
    1.21    | is_f_x _ = false;
    1.22  (* precondition: TermC.is_atom v andalso TermC.is_atom c *)
    1.23 +fun is_const (Const _) = true | is_const _ = false;
    1.24  fun variable_constant_pair (v, c) =
    1.25    if (is_variable v andalso (is_const c orelse is_num c)) orelse
    1.26       (is_variable c andalso (is_const v orelse is_num v))

     2.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Wed Aug 18 11:35:24 2021 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Wed Aug 18 16:03:08 2021 +0200
     2.3 @@ -29,7 +29,6 @@
     2.4  calculation some_occur_in = \<open>Prog_Expr.eval_some_occur_in "#some_occur_in_"\<close>
     2.5  calculation is_atom = \<open>Prog_Expr.eval_is_atom "#is_atom_"\<close>
     2.6  calculation is_even = \<open>Prog_Expr.eval_is_even "#is_even_"\<close>
     2.7 -calculation is_const = \<open>Prog_Expr.eval_const "#is_const_"\<close>
     2.8  calculation le (less) = \<open>Prog_Expr.eval_equ "#less_"\<close>
     2.9  calculation leq (less_eq) = \<open>Prog_Expr.eval_equ "#less_equal_"\<close>
    2.10  calculation ident = \<open>Prog_Expr.eval_ident "#ident_"\<close>
    2.11 @@ -82,7 +81,7 @@
    2.12  	\<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
    2.13  	
    2.14  	\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
    2.15 -	\<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
    2.16 +	\<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
    2.17  	\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
    2.18  	\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];
    2.19  \<close>
    2.20 @@ -108,7 +107,7 @@
    2.21   	\<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
    2.22   	
    2.23   	\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
    2.24 - 	\<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
    2.25 +	\<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
    2.26   	\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
    2.27   	\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];
    2.28  \<close>

     3.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Wed Aug 18 11:35:24 2021 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Wed Aug 18 16:03:08 2021 +0200
     3.3 @@ -136,6 +136,7 @@
     3.4    erls = Rule_Set.append_rules "erls_diff_sym_conv" Rule_Set.empty [
     3.5      \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), 
     3.6      \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
     3.7 +    \<^rule_eval>\<open>is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"),
     3.8      \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
     3.9      \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
    3.10      \<^rule_thm>\<open>not_false\<close>,
    3.11 @@ -145,7 +146,7 @@
    3.12      \<^rule_thm>\<open>frac_sym_conv\<close>,
    3.13      \<^rule_thm>\<open>sqrt_sym_conv\<close>,
    3.14      \<^rule_thm>\<open>root_sym_conv\<close>,
    3.15 -    \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*),
    3.16 +    \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_atom) ==> - (z::real) = -1 * z"*),
    3.17      \<^rule_thm>\<open>minus_minus\<close> (*"- (- ?a) = ?a"*),
    3.18      \<^rule_thm>\<open>rat_mult\<close> (*a / b * (c / d) = a * c / (b * d)*),
    3.19      \<^rule_thm>\<open>times_divide_eq_right\<close> (*?x * (?y / ?z) = ?x * ?y / ?z*),
    3.20 @@ -173,7 +174,7 @@
    3.21  		\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
    3.22  		\<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"),
    3.23  		\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
    3.24 -		\<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_")];
    3.25 +  	\<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")];
    3.26  
    3.27  (*.rules for differentiation, _no_ simplification.*)
    3.28  val diff_rules =

     4.1 --- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml	Wed Aug 18 11:35:24 2021 +0200
     4.2 +++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml	Wed Aug 18 16:03:08 2021 +0200
     4.3 @@ -195,7 +195,7 @@
     4.4  val given  = ["formula_for_max (lhs=rhs)", "boundVariable bdv",
     4.5  	      "interval {x. low < x & x < high}",
     4.6  	      "additional_conds ac", "constants cs"];
     4.7 -val where_ = ["lhs is_const", "bdv is_const", "low is_const", "high is_const",
     4.8 +val where_ = ["lhs is_atom", "bdv is_atom", "low is_atom", "high is_atom",
     4.9  	      "||| Vars equ ||| = ||| VarsSet ac ||| - ||| ac ||| + #1"];
    4.10  val find   = ["f::real => real", "maxs::real set"];
    4.11  val with_  = [(* incompat.w. parse, ok with parseold
    4.12 @@ -248,7 +248,7 @@
    4.13  val given  = ["equation (lhs=rhs)",
    4.14  	      "interval {x. low < x & x < high}",
    4.15  	      "constants cs"];
    4.16 -val where_ = ["lhs is_const", "low is_const", "high is_const"];
    4.17 +val where_ = ["lhs is_atom", "low is_atom", "high is_atom"];
    4.18  val find   = ["t::real"];
    4.19  val with_  = ["||| Vars t ||| = #1"];
    4.20  val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
    4.21 @@ -263,7 +263,7 @@
    4.22  
    4.23  val given  = ["functionTerm t",
    4.24  	      "boundVariable bdv"];
    4.25 -val where_ = ["bdv is_const"];
    4.26 +val where_ = ["bdv is_atom"];
    4.27  val find   = ["t'::real"];
    4.28  val with_  = ["t' is_derivative_of (%bdv. t)"];
    4.29  val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
    4.30 @@ -281,11 +281,11 @@
    4.31  val given  = ["equation (a*(cos bdv) \<up> #2 + b*(cos bdv)*(sin bdv) + \
    4.32  	      \ c*(sin bdv) = #0)",
    4.33  	     "boundVariable bdv", "errorBound epsilon"];
    4.34 -val where_ = ["bdv is_const", "epsilon is_const_expr"];
    4.35 +val where_ = ["bdv is_atom", "epsilon is_const_expr"];
    4.36  val find   = ["L::real set"];
    4.37  val with_  = ["L = {x. || (%bdv. a*(cos bdv) \<up> #2 + b*(cos bdv)*(sin bdv) + \
    4.38  	      \ c*(sin bdv)) x || < epsilon}"];
    4.39 -(* 5.3.00
    4.40 +(* 5.3.00                         
    4.41  val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
    4.42  val givens = map (the o (parse thy)) given;
    4.43  val tag__forms = chktyps thy (formals, givens);

     5.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy	Wed Aug 18 11:35:24 2021 +0200
     5.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy	Wed Aug 18 16:03:08 2021 +0200
     5.3 @@ -51,7 +51,7 @@
     5.4        \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
     5.5        
     5.6        \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),    
     5.7 -      \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
     5.8 +    	\<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
     5.9        \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),    
    5.10        \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")],
    5.11      scr = Rule.Empty_Prog

     6.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Wed Aug 18 11:35:24 2021 +0200
     6.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Wed Aug 18 16:03:08 2021 +0200
     6.3 @@ -109,7 +109,7 @@
     6.4    real_minus_binom_pow3:   "(a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3" and
     6.5    real_minus_binom_pow3_p: "(a + -1 * b) \<up> 3 = a \<up> 3 + -3*a \<up> 2*b + 3*a*b \<up> 2 +
     6.6                             -1*b \<up> 3" and
     6.7 -(* real_plus_binom_pow:        "[| n is_const;  3 < n |] ==>
     6.8 +(* real_plus_binom_pow:        "[| n is_num;  3 < n |] ==>
     6.9  			       (a + b) \<up> n = (a + b) * (a + b)\<up>(n - 1)" *)
    6.10    real_plus_binom_pow4:   "(a + b) \<up> 4 = (a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3)
    6.11                             *(a + b)" and
    6.12 @@ -142,24 +142,24 @@
    6.13    real_plus_binom_times1:     "(a +  1*b)*(a + -1*b) = a \<up> 2 + -1*b \<up> 2" and
    6.14    real_plus_binom_times2:     "(a + -1*b)*(a +  1*b) = a \<up> 2 + -1*b \<up> 2" and
    6.15  
    6.16 -  real_num_collect:           "[| l is_const; m is_const |] ==>
    6.17 +  real_num_collect:           "[| l is_num; m is_num |] ==>
    6.18  			      l * n + m * n = (l + m) * n" and
    6.19  (* FIXME.MG.0401: replace 'real_num_collect_assoc' 
    6.20  	by 'real_num_collect_assoc_l' ... are equal, introduced by MG ! *)
    6.21 -  real_num_collect_assoc:     "[| l is_const; m is_const |] ==> 
    6.22 +  real_num_collect_assoc:     "[| l is_num; m is_num |] ==> 
    6.23  			      l * n + (m * n + k) = (l + m) * n + k" and
    6.24 -  real_num_collect_assoc_l:   "[| l is_const; m is_const |] ==>
    6.25 +  real_num_collect_assoc_l:   "[| l is_num; m is_num |] ==>
    6.26  			      l * n + (m * n + k) = (l + m)
    6.27  				* n + k" and
    6.28 -  real_num_collect_assoc_r:   "[| l is_const; m is_const |] ==>
    6.29 +  real_num_collect_assoc_r:   "[| l is_num; m is_num |] ==>
    6.30  			      (k + m * n) + l * n = k + (l + m) * n" and
    6.31 -  real_one_collect:           "m is_const ==> n + m * n = (1 + m) * n" and
    6.32 +  real_one_collect:           "m is_num ==> n + m * n = (1 + m) * n" and
    6.33  (* FIXME.MG.0401: replace 'real_one_collect_assoc' 
    6.34  	by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *)
    6.35 -  real_one_collect_assoc:     "m is_const ==> n + (m * n + k) = (1 + m)* n + k" and
    6.36 +  real_one_collect_assoc:     "m is_num ==> n + (m * n + k) = (1 + m)* n + k" and
    6.37  
    6.38 -  real_one_collect_assoc_l:   "m is_const ==> n + (m * n + k) = (1 + m) * n + k" and
    6.39 -  real_one_collect_assoc_r:  "m is_const ==> (k + n) +  m * n = k + (1 + m) * n" and
    6.40 +  real_one_collect_assoc_l:   "m is_num ==> n + (m * n + k) = (1 + m) * n + k" and
    6.41 +  real_one_collect_assoc_r:  "m is_num ==> (k + n) +  m * n = k + (1 + m) * n" and
    6.42  
    6.43  (* FIXME.MG.0401: replace 'real_mult_2_assoc' 
    6.44  	by 'real_mult_2_assoc_l' ... are equal, introduced by MG ! *)
    6.45 @@ -730,6 +730,9 @@
    6.46  	      \<^rule_thm>\<open>distrib_left\<close> (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)],
    6.47        scr = Rule.Empty_Prog};
    6.48  
    6.49 +\<close> ML \<open>
    6.50 +\<close> ML \<open>@{term "1 is_num"}\<close>
    6.51 +ML \<open>
    6.52  (* erls for calculate_Rational + etc *)
    6.53  val powers_erls =
    6.54    Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
    6.55 @@ -751,7 +754,7 @@
    6.56        erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    6.57        rules = [
    6.58          \<^rule_thm>\<open>real_diff_minus\<close> (*"a - b = a + -1 * b"*),
    6.59 -        \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)],
    6.60 +        \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_num) ==> - (z::real) = -1 * z"*)],
    6.61  	    scr = Rule.Empty_Prog};
    6.62  
    6.63  val expand_poly_ = 
    6.64 @@ -865,11 +868,11 @@
    6.65        calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_"))
    6.66  	      ], errpatts = [],
    6.67        rules = [
    6.68 -        \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
    6.69 +        \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
    6.70  	      \<^rule_thm>\<open>real_num_collect_assoc_r\<close>,
    6.71 -	        (*"[| l is_const; m is_const |] ==> (k + m * n) + l * n = k + (l + m)*n"*)
    6.72 -        \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_const ==> n + m * n = (1 + m) * n"*)
    6.73 -        \<^rule_thm>\<open>real_one_collect_assoc_r\<close>, (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
    6.74 +	        (*"[| l is_num; m is_num |] ==> (k + m * n) + l * n = k + (l + m)*n"*)
    6.75 +        \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
    6.76 +        \<^rule_thm>\<open>real_one_collect_assoc_r\<close>, (*"m is_num ==> (k + n) + m * n = k + (m + 1) * n"*)
    6.77  
    6.78          \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
    6.79  
    6.80 @@ -914,7 +917,7 @@
    6.81  
    6.82          \<^rule_thm>\<open>minus_minus\<close> (*"- (- ?z) = ?z"*),
    6.83          \<^rule_thm>\<open>real_diff_minus\<close> (*"a - b = a + -1 * b"*),
    6.84 -        \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)
    6.85 +        \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_num) ==> - (z::real) = -1 * z"*)
    6.86  
    6.87  	       (*\<^rule_thm>\<open>real_minus_add_distrib\<close>,*) (*"- (?x + ?y) = - ?x + - ?y"*)
    6.88  	       (*\<^rule_thm>\<open>real_diff_plus\<close>*) (*"a - b = a + -b"*)],
    6.89 @@ -945,11 +948,11 @@
    6.90  	      ("POWER", (\<^const_name>\<open>powr\<close>, eval_binop "#power_"))
    6.91  	      ], errpatts = [],
    6.92        rules =[
    6.93 -        \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
    6.94 +        \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
    6.95  	      \<^rule_thm>\<open>real_num_collect_assoc\<close>,
    6.96 -          (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) =  (l + m) * n + k"*)
    6.97 -	      \<^rule_thm>\<open>real_one_collect\<close>,	 (*"m is_const ==> n + m * n = (1 + m) * n"*)
    6.98 -	      \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
    6.99 +          (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) =  (l + m) * n + k"*)
   6.100 +	      \<^rule_thm>\<open>real_one_collect\<close>,	 (*"m is_num ==> n + m * n = (1 + m) * n"*)
   6.101 +	      \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
   6.102  	      \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), 
   6.103  	      \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
   6.104  	      \<^rule_eval>\<open>powr\<close> (eval_binop "#power_")],
   6.105 @@ -1194,10 +1197,10 @@
   6.106  	     \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)
   6.107  	     \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*)
   6.108  
   6.109 -	     \<^rule_thm>\<open>real_num_collect\<close>,  (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
   6.110 -	     \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) =  (l + m) * n + k"*)
   6.111 -	     \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_const ==> n + m * n = (1 + m) * n"*)
   6.112 -	     \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
   6.113 +	     \<^rule_thm>\<open>real_num_collect\<close>,  (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
   6.114 +	     \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) =  (l + m) * n + k"*)
   6.115 +	     \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
   6.116 +	     \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
   6.117  
   6.118  	     \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
   6.119  
   6.120 @@ -1299,10 +1302,10 @@
   6.121         \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)*)
   6.122  	     \<^rule_thm>\<open>real_mult_2_assoc\<close>,	 (*"z1 + (z1 + k) = 2 * z1 + k"*)
   6.123      
   6.124 -	     \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
   6.125 -	     \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) =  (l + m) * n + k"*)
   6.126 -	     \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_const ==> n + m * n = (1 + m) * n"*)
   6.127 -	     \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
   6.128 +	     \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |] ==>l * n + m * n = (l + m) * n"*)
   6.129 +	     \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) =  (l + m) * n + k"*)
   6.130 +	     \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
   6.131 +	     \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
   6.132      
   6.133  	     \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), 
   6.134  	     \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
   6.135 @@ -1314,9 +1317,14 @@
   6.136  subsubsection \<open>rule-sets\<close>
   6.137  ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory}\<close>
   6.138  
   6.139 +ML \<open>@{term "1 is_num"}\<close> (*.."Prog_Expr.is_num" IS KNOWN TOODOO*)
   6.140  rule_set_knowledge
   6.141 -  norm_Poly = \<open>prep_rls' norm_Poly\<close> and
   6.142 -  Poly_erls = \<open>prep_rls' Poly_erls\<close> (*FIXXXME:del with rls.rls'*) and
   6.143 +  norm_Poly = \<open>prep_rls' norm_Poly\<close> 
   6.144 +(*/---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------\* )
   6.145 +and
   6.146 +  Poly_erls = \<open>prep_rls' Poly_erls\<close> (*FIXXXME:del with rls.rls'*) 
   6.147 +( *\---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------/*)
   6.148 +and
   6.149    expand = \<open>prep_rls' expand\<close> and
   6.150    expand_poly = \<open>prep_rls' expand_poly\<close> and
   6.151    simplify_power = \<open>prep_rls' simplify_power\<close> and
   6.152 @@ -1370,7 +1378,6 @@
   6.153    Given: "Term t_t"
   6.154    Where: "t_t is_polyexp"
   6.155    Find: "normalform n_n"
   6.156 -
   6.157  ML \<open>
   6.158  \<close> ML \<open>
   6.159  \<close> 

     7.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy	Wed Aug 18 11:35:24 2021 +0200
     7.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Wed Aug 18 16:03:08 2021 +0200
     7.3 @@ -51,42 +51,42 @@
     7.4    x_quadrat:             "(x * a) * a = x * a \<up> 2" and
     7.5  
     7.6  
     7.7 -  subtrahiere:               "[| l is_const; m is_const |] ==>  
     7.8 +  subtrahiere:               "[| l is_num; m is_num |] ==>  
     7.9  			     m * v - l * v = (m - l) * v" and
    7.10 -  subtrahiere_von_1:         "[| l is_const |] ==>  
    7.11 +  subtrahiere_von_1:         "[| l is_num |] ==>  
    7.12  			     v - l * v = (1 - l) * v" and
    7.13 -  subtrahiere_1:             "[| l is_const; m is_const |] ==>  
    7.14 +  subtrahiere_1:             "[| l is_num; m is_num |] ==>  
    7.15  			     m * v - v = (m - 1) * v" and
    7.16  
    7.17 -  subtrahiere_x_plus_minus:  "[| l is_const; m is_const |] ==>  
    7.18 +  subtrahiere_x_plus_minus:  "[| l is_num; m is_num |] ==>  
    7.19  			     (x + m * v) - l * v = x + (m - l) * v" and
    7.20 -  subtrahiere_x_plus1_minus: "[| l is_const |] ==>  
    7.21 +  subtrahiere_x_plus1_minus: "[| l is_num |] ==>  
    7.22  			     (x + v) - l * v = x + (1 - l) * v" and
    7.23 -  subtrahiere_x_plus_minus1: "[| m is_const |] ==>  
    7.24 +  subtrahiere_x_plus_minus1: "[| m is_num |] ==>  
    7.25  			     (x + m * v) - v = x + (m - 1) * v" and
    7.26  
    7.27 -  subtrahiere_x_minus_plus:  "[| l is_const; m is_const |] ==>  
    7.28 +  subtrahiere_x_minus_plus:  "[| l is_num; m is_num |] ==>  
    7.29  			     (x - m * v) + l * v = x + (-m + l) * v" and
    7.30 -  subtrahiere_x_minus1_plus: "[| l is_const |] ==>  
    7.31 +  subtrahiere_x_minus1_plus: "[| l is_num |] ==>  
    7.32  			     (x - v) + l * v = x + (-1 + l) * v" and
    7.33 -  subtrahiere_x_minus_plus1: "[| m is_const |] ==>  
    7.34 +  subtrahiere_x_minus_plus1: "[| m is_num |] ==>  
    7.35  			     (x - m * v) + v = x + (-m + 1) * v" and
    7.36  
    7.37 -  subtrahiere_x_minus_minus: "[| l is_const; m is_const |] ==>  
    7.38 +  subtrahiere_x_minus_minus: "[| l is_num; m is_num |] ==>  
    7.39  			     (x - m * v) - l * v = x + (-m - l) * v" and
    7.40 -  subtrahiere_x_minus1_minus:"[| l is_const |] ==>  
    7.41 +  subtrahiere_x_minus1_minus:"[| l is_num |] ==>  
    7.42  			     (x - v) - l * v = x + (-1 - l) * v" and
    7.43 -  subtrahiere_x_minus_minus1:"[| m is_const |] ==>  
    7.44 +  subtrahiere_x_minus_minus1:"[| m is_num |] ==>  
    7.45  			     (x - m * v) - v = x + (-m - 1) * v" and
    7.46  
    7.47  
    7.48 -  addiere_vor_minus:         "[| l is_const; m is_const |] ==>  
    7.49 +  addiere_vor_minus:         "[| l is_num; m is_num |] ==>  
    7.50  			     - (l * v) +  m * v = (-l + m) * v" and
    7.51 -  addiere_eins_vor_minus:    "[| m is_const |] ==>  
    7.52 +  addiere_eins_vor_minus:    "[| m is_num |] ==>  
    7.53  			     -  v +  m * v = (-1 + m) * v" and
    7.54 -  subtrahiere_vor_minus:     "[| l is_const; m is_const |] ==>  
    7.55 +  subtrahiere_vor_minus:     "[| l is_num; m is_num |] ==>  
    7.56  			     - (l * v) -  m * v = (-l - m) * v" and
    7.57 -  subtrahiere_eins_vor_minus:"[| m is_const |] ==>  
    7.58 +  subtrahiere_eins_vor_minus:"[| m is_num |] ==>  
    7.59  			     -  v -  m * v = (-1 - m) * v" and
    7.60  
    7.61  (*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)
    7.62 @@ -208,29 +208,29 @@
    7.63    Rule_Def.Repeat{id = "fasse_zusammen", preconds = [], 
    7.64  	  rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
    7.65  	  erls = Rule_Set.append_rules "erls_fasse_zusammen" Rule_Set.empty 
    7.66 -	  	[\<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_")],
    7.67 +	  	[\<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")],
    7.68  	  srls = Rule_Set.Empty, calc = [], errpatts = [],
    7.69  	  rules = [
    7.70 -     \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
    7.71 -  	 \<^rule_thm>\<open>real_num_collect_assoc_r\<close>, (*"[| l is_const; m..|] ==>  (k + m * n) + l * n = k + (l + m)*n"*)
    7.72 -  	 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_const ==> n + m * n = (1 + m) * n"*)
    7.73 -  	 \<^rule_thm>\<open>real_one_collect_assoc_r\<close>, (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
    7.74 +     \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
    7.75 +  	 \<^rule_thm>\<open>real_num_collect_assoc_r\<close>, (*"[| l is_num; m..|] ==>  (k + m * n) + l * n = k + (l + m)*n"*)
    7.76 +  	 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
    7.77 +  	 \<^rule_thm>\<open>real_one_collect_assoc_r\<close>, (*"m is_num ==> (k + n) + m * n = k + (m + 1) * n"*)
    7.78  
    7.79 -  	 \<^rule_thm>\<open>subtrahiere\<close>, (*"[| l is_const; m is_const |] ==> m * v - l * v = (m - l) * v"*)
    7.80 -  	 \<^rule_thm>\<open>subtrahiere_von_1\<close>, (*"[| l is_const |] ==> v - l * v = (1 - l) * v"*)
    7.81 -  	 \<^rule_thm>\<open>subtrahiere_1\<close>, (*"[| l is_const; m is_const |] ==> m * v - v = (m - 1) * v"*)
    7.82 +  	 \<^rule_thm>\<open>subtrahiere\<close>, (*"[| l is_num; m is_num |] ==> m * v - l * v = (m - l) * v"*)
    7.83 +  	 \<^rule_thm>\<open>subtrahiere_von_1\<close>, (*"[| l is_num |] ==> v - l * v = (1 - l) * v"*)
    7.84 +  	 \<^rule_thm>\<open>subtrahiere_1\<close>, (*"[| l is_num; m is_num |] ==> m * v - v = (m - 1) * v"*)
    7.85  
    7.86 -  	 \<^rule_thm>\<open>subtrahiere_x_plus_minus\<close>, (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
    7.87 -  	 \<^rule_thm>\<open>subtrahiere_x_plus1_minus\<close>, (*"[| l is_const |] ==> (x + v) - l * v = x + (1 - l) * v"*)
    7.88 -  	 \<^rule_thm>\<open>subtrahiere_x_plus_minus1\<close>, (*"[| m is_const |] ==> (x + m * v) - v = x + (m - 1) * v"*)
    7.89 +  	 \<^rule_thm>\<open>subtrahiere_x_plus_minus\<close>, (*"[| l is_num; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
    7.90 +  	 \<^rule_thm>\<open>subtrahiere_x_plus1_minus\<close>, (*"[| l is_num |] ==> (x + v) - l * v = x + (1 - l) * v"*)
    7.91 +  	 \<^rule_thm>\<open>subtrahiere_x_plus_minus1\<close>, (*"[| m is_num |] ==> (x + m * v) - v = x + (m - 1) * v"*)
    7.92  
    7.93 -  	 \<^rule_thm>\<open>subtrahiere_x_minus_plus\<close>, (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
    7.94 -  	 \<^rule_thm>\<open>subtrahiere_x_minus1_plus\<close>, (*"[| l is_const |] ==> (x - v) + l * v = x + (-1 + l) * v"*)
    7.95 -  	 \<^rule_thm>\<open>subtrahiere_x_minus_plus1\<close>, (*"[| m is_const |] ==> (x - m * v) + v = x + (-m + 1) * v"*)
    7.96 +  	 \<^rule_thm>\<open>subtrahiere_x_minus_plus\<close>, (*"[| l is_num; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
    7.97 +  	 \<^rule_thm>\<open>subtrahiere_x_minus1_plus\<close>, (*"[| l is_num |] ==> (x - v) + l * v = x + (-1 + l) * v"*)
    7.98 +  	 \<^rule_thm>\<open>subtrahiere_x_minus_plus1\<close>, (*"[| m is_num |] ==> (x - m * v) + v = x + (-m + 1) * v"*)
    7.99  
   7.100 -  	 \<^rule_thm>\<open>subtrahiere_x_minus_minus\<close>, (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)
   7.101 -  	 \<^rule_thm>\<open>subtrahiere_x_minus1_minus\<close>, (*"[| l is_const |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
   7.102 -  	 \<^rule_thm>\<open>subtrahiere_x_minus_minus1\<close>, (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
   7.103 +  	 \<^rule_thm>\<open>subtrahiere_x_minus_minus\<close>, (*"[| l is_num; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)
   7.104 +  	 \<^rule_thm>\<open>subtrahiere_x_minus1_minus\<close>, (*"[| l is_num |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
   7.105 +  	 \<^rule_thm>\<open>subtrahiere_x_minus_minus1\<close>, (*"[| m is_num |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
   7.106  
   7.107    	 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
   7.108    	 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_"),
   7.109 @@ -240,10 +240,10 @@
   7.110    	 \<^rule_thm>\<open>real_mult_2_assoc_r\<close>, (*"(k + z1) + z1 = k + 2 * z1"*)
   7.111    	 \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)
   7.112  
   7.113 -  	 \<^rule_thm>\<open>addiere_vor_minus\<close>, (*"[| l is_const; m is_const |] ==> -(l * v) +  m * v = (-l + m) *v"*)
   7.114 -  	 \<^rule_thm>\<open>addiere_eins_vor_minus\<close>, (*"[| m is_const |] ==> -  v +  m * v = (-1 + m) * v"*)
   7.115 -  	 \<^rule_thm>\<open>subtrahiere_vor_minus\<close>, (*"[| l is_const; m is_const |] ==> -(l * v) -  m * v = (-l - m) *v"*)
   7.116 -  	 \<^rule_thm>\<open>subtrahiere_eins_vor_minus\<close>], (*"[| m is_const |] ==> -  v -  m * v = (-1 - m) * v"*)	 
   7.117 +  	 \<^rule_thm>\<open>addiere_vor_minus\<close>, (*"[| l is_num; m is_num |] ==> -(l * v) +  m * v = (-l + m) *v"*)
   7.118 +  	 \<^rule_thm>\<open>addiere_eins_vor_minus\<close>, (*"[| m is_num |] ==> -  v +  m * v = (-1 + m) * v"*)
   7.119 +  	 \<^rule_thm>\<open>subtrahiere_vor_minus\<close>, (*"[| l is_num; m is_num |] ==> -(l * v) -  m * v = (-l - m) *v"*)
   7.120 +  	 \<^rule_thm>\<open>subtrahiere_eins_vor_minus\<close>], (*"[| m is_num |] ==> -  v -  m * v = (-1 - m) * v"*)	 
   7.121  	  scr = Rule.Empty_Prog};
   7.122      
   7.123  val verschoenere = 

     8.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Wed Aug 18 11:35:24 2021 +0200
     8.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Wed Aug 18 16:03:08 2021 +0200
     8.3 @@ -89,7 +89,7 @@
     8.4  
     8.5  (*real_times_divide1_eq .. Isa02*) 
     8.6    real_times_divide_1_eq:  "-1 * (c / d) = -1 * c / d " and
     8.7 -  real_times_divide_num:   "a is_const ==> a * (c / d) = a * c / d " and
     8.8 +  real_times_divide_num:   "a is_num ==> a * (c / d) = a * c / d " and
     8.9  
    8.10    real_mult_div_cancel2:   "k ~= 0 ==> m * k / (n * k) = m / n" and
    8.11  (*real_mult_div_cancel1:   "k ~= 0 ==> k * m / (k * n) = m / n"..Isa02*)
    8.12 @@ -100,21 +100,21 @@
    8.13  			  
    8.14    rat_power:               "(a / b) \<up> n = (a \<up> n) / (b \<up> n)" and
    8.15  
    8.16 -  rat_add:         "[| a is_const; b is_const; c is_const; d is_const |] ==> 
    8.17 +  rat_add:         "[| a is_num; b is_num; c is_num; d is_num |] ==> 
    8.18  	           a / c + b / d = (a * d + b * c) / (c * d)" and
    8.19 -  rat_add_assoc:   "[| a is_const; b is_const; c is_const; d is_const |] ==> 
    8.20 +  rat_add_assoc:   "[| a is_num; b is_num; c is_num; d is_num |] ==> 
    8.21  	           a / c +(b / d + e) = (a * d + b * c)/(d * c) + e" and
    8.22 -  rat_add1:        "[| a is_const; b is_const; c is_const |] ==> 
    8.23 +  rat_add1:        "[| a is_num; b is_num; c is_num |] ==> 
    8.24  	           a / c + b / c = (a + b) / c" and
    8.25 -  rat_add1_assoc:   "[| a is_const; b is_const; c is_const |] ==> 
    8.26 +  rat_add1_assoc:   "[| a is_num; b is_num; c is_num |] ==> 
    8.27  	           a / c + (b / c + e) = (a + b) / c + e" and
    8.28 -  rat_add2:        "[| a is_const; b is_const; c is_const |] ==> 
    8.29 +  rat_add2:        "[| a is_num; b is_num; c is_num |] ==> 
    8.30  	           a / c + b = (a + b * c) / c" and
    8.31 -  rat_add2_assoc:  "[| a is_const; b is_const; c is_const |] ==> 
    8.32 +  rat_add2_assoc:  "[| a is_num; b is_num; c is_num |] ==> 
    8.33  	           a / c + (b + e) = (a + b * c) / c + e" and
    8.34 -  rat_add3:        "[| a is_const; b is_const; c is_const |] ==> 
    8.35 +  rat_add3:        "[| a is_num; b is_num; c is_num |] ==> 
    8.36  	           a + b / c = (a * c + b) / c" and
    8.37 -  rat_add3_assoc:   "[| a is_const; b is_const; c is_const |] ==> 
    8.38 +  rat_add3_assoc:   "[| a is_num; b is_num; c is_num |] ==> 
    8.39  	           a + (b / c + e) = (a * c + b) / c + e"
    8.40  
    8.41  section \<open>Cancellation and addition of fractions\<close>
    8.42 @@ -414,7 +414,9 @@
    8.43        rules = [
    8.44          \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
    8.45          \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
    8.46 -        \<^rule_eval>\<open>is_const\<close> (Prog_Expr.eval_const "#is_const_"),
    8.47 +(*/----- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly -------\* )
    8.48 +        \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
    8.49 +( *\---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------/*)
    8.50          \<^rule_thm>\<open>not_true\<close>,
    8.51          \<^rule_thm>\<open>not_false\<close>], 
    8.52        scr = Rule.Empty_Prog});
    8.53 @@ -432,10 +434,10 @@
    8.54  
    8.55          \<^rule_thm_sym>\<open>minus_divide_left\<close>, (*SYM - ?x / ?y = - (?x / ?y)  may come from subst*)
    8.56          \<^rule_thm>\<open>rat_add\<close>,
    8.57 -          (*"[| a is_const; b is_const; c is_const; d is_const |] ==> a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
    8.58 -        \<^rule_thm>\<open>rat_add1\<close>, (*"[| a is_const; b is_const; c is_const |] ==> a / c + b / c = (a + b) / c"*)
    8.59 -        \<^rule_thm>\<open>rat_add2\<close>, (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
    8.60 -        \<^rule_thm>\<open>rat_add3\<close>, (*"[| a is_const; b is_const; c is_const |] ==> a + b / c = (a * c) / c + b / c" *)
    8.61 +          (*"[| a is_num; b is_num; c is_num; d is_num |] ==> a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
    8.62 +        \<^rule_thm>\<open>rat_add1\<close>, (*"[| a is_num; b is_num; c is_num |] ==> a / c + b / c = (a + b) / c"*)
    8.63 +        \<^rule_thm>\<open>rat_add2\<close>, (*"[| ?a is_num; ?b is_num; ?c is_num |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
    8.64 +        \<^rule_thm>\<open>rat_add3\<close>, (*"[| a is_num; b is_num; c is_num |] ==> a + b / c = (a * c) / c + b / c" *)
    8.65          
    8.66          \<^rule_thm>\<open>rat_mult\<close>, (*a / b * (c / d) = a * c / (b * d)*)
    8.67          \<^rule_thm>\<open>times_divide_eq_right\<close>, (*?x * (?y / ?z) = ?x * ?y / ?z*)
    8.68 @@ -626,6 +628,7 @@
    8.69          \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
    8.70        scr = Rule.Empty_Prog});
    8.71  
    8.72 +\<close> ML \<open>
    8.73  (*.contains absolute minimum of thms for context in norm_Rational.*)
    8.74  val rat_mult_divide = prep_rls'(
    8.75    Rule_Def.Repeat {id = "rat_mult_divide", preconds = [], 
    8.76 @@ -643,6 +646,7 @@
    8.77  	       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")],
    8.78        scr = Rule.Empty_Prog});
    8.79  
    8.80 +\<close> ML \<open>
    8.81  (*.contains absolute minimum of thms for context in norm_Rational.*)
    8.82  val reduce_0_1_2 = prep_rls'(
    8.83    Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
    8.84 @@ -664,15 +668,23 @@
    8.85        \<^rule_thm>\<open>division_ring_divide_zero\<close> (*"0 / ?x = 0"*)],
    8.86      scr = Rule.Empty_Prog});
    8.87  
    8.88 +\<close> ML \<open>
    8.89 +\<close> ML \<open>@{term "1 is_num"}\<close> (*.."Prog_Expr.is_num" IS KNOWN TOODOO*)
    8.90 +ML \<open>
    8.91  (*erls for calculate_Rational; 
    8.92    make local with FIXX@ME result:term *term list WN0609???SKMG*)
    8.93  val norm_rat_erls = prep_rls'(
    8.94    Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
    8.95      erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
    8.96      rules = [
    8.97 -      \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_")],
    8.98 +      \<^rule_thm>\<open>refl\<close> (* ..DELETE, just to avoid ERROR fun #> not applicable to "[]"*)
    8.99 +(*/----- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly -------\* )
   8.100 +      \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")
   8.101 +( *\---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------/*)
   8.102 +],
   8.103      scr = Rule.Empty_Prog});
   8.104  
   8.105 +\<close> ML \<open>
   8.106  (* consists of rls containing the absolute minimum of thms *)
   8.107  (*
   8.108    which is now replaced by MGs version "norm_Rational" below
   8.109 @@ -693,6 +705,7 @@
   8.110  	     ],
   8.111      scr = Rule.Empty_Prog});
   8.112  
   8.113 +\<close> ML \<open>
   8.114  val norm_Rational_parenthesized = prep_rls'(
   8.115    Rule_Set.Sequence {id = "norm_Rational_parenthesized", preconds = []:term list, 
   8.116      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),

     9.1 --- a/src/Tools/isac/Knowledge/Root.thy	Wed Aug 18 11:35:24 2021 +0200
     9.2 +++ b/src/Tools/isac/Knowledge/Root.thy	Wed Aug 18 16:03:08 2021 +0200
     9.3 @@ -216,10 +216,10 @@
     9.4        \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)
     9.5        \<^rule_thm>\<open>real_mult_2_assoc\<close>,	(*"z1 + (z1 + k) = 2 * z1 + k"*)
     9.6  
     9.7 -      \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_const; m is_const |]==> l * n + m * n = (l + m) * n"*)
     9.8 -      \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) =  (l + m) * n + k"*)
     9.9 -      \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_const ==> n + m * n = (1 + m) * n"*)
    9.10 -      \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
    9.11 +      \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==> l * n + m * n = (l + m) * n"*)
    9.12 +      \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) =  (l + m) * n + k"*)
    9.13 +      \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
    9.14 +      \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
    9.15  
    9.16        \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
    9.17        \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
    9.18 @@ -264,10 +264,10 @@
    9.19         \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r  \<up>  n = r  \<up>  (n + 1)"*)
    9.20         \<^rule_thm>\<open>real_mult_2_assoc\<close>,	 (*"z1 + (z1 + k) = 2 * z1 + k"*)
    9.21    
    9.22 -       \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
    9.23 -       \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) =  (l + m) * n + k"*)
    9.24 -       \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_const ==> n + m * n = (1 + m) * n"*)
    9.25 -       \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
    9.26 +       \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |] ==>l * n + m * n = (l + m) * n"*)
    9.27 +       \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) =  (l + m) * n + k"*)
    9.28 +       \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
    9.29 +       \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
    9.30    
    9.31         \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
    9.32         \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"), 

    10.1 --- a/src/Tools/isac/Knowledge/RootRat.thy	Wed Aug 18 11:35:24 2021 +0200
    10.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy	Wed Aug 18 16:03:08 2021 +0200
    10.3 @@ -16,7 +16,7 @@
    10.4    Rule_Set.append_rules "calculate_RootRat" calculate_Rational [
    10.5      \<^rule_thm>\<open>distrib_left\<close> (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *),
    10.6  		\<^rule_thm>\<open>mult_1_left\<close> (* 1 * z = z *),
    10.7 -    \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*),
    10.8 +    \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_num) ==> - (z::real) = -1 * z"*),
    10.9  		\<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_")];
   10.10  
   10.11  val prep_rls' = Auto_Prog.prep_rls @{theory};

    11.1 --- a/src/Tools/isac/Knowledge/Test.thy	Wed Aug 18 11:35:24 2021 +0200
    11.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Wed Aug 18 16:03:08 2021 +0200
    11.3 @@ -149,20 +149,20 @@
    11.4    rdistr_right_assoc_p:    "l * n + (m * n + (k::real)) = (l + m) * n + k" and
    11.5    rdistr_div_right:        "((k::real) + l) / n = k / n + l / n" and
    11.6    rcollect_right:
    11.7 -          "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n" and
    11.8 +          "[| l is_num; m is_num |] ==> (l::real)*n + m*n = (l + m) * n" and
    11.9    rcollect_one_left:
   11.10 -          "m is_const ==> (n::real) + m * n = (1 + m) * n" and
   11.11 +          "m is_num ==> (n::real) + m * n = (1 + m) * n" and
   11.12    rcollect_one_left_assoc:
   11.13 -          "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n" and
   11.14 +          "m is_num ==> (k::real) + n + m * n = k + (1 + m) * n" and
   11.15    rcollect_one_left_assoc_p:
   11.16 -          "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k" and
   11.17 +          "m is_num ==> n + (m * n + (k::real)) = (1 + m) * n + k" and
   11.18  
   11.19    rtwo_of_the_same:        "a + a = 2 * a" and
   11.20    rtwo_of_the_same_assoc:  "(x + a) + a = x + 2 * a" and
   11.21    rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x" and
   11.22  
   11.23    rcancel_den:             "a \<noteq> 0 ==> a * (b / a) = b" and
   11.24 -  rcancel_const:           "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x" and
   11.25 +  rcancel_const:           "[| a is_num; b is_num |] ==> a*(x/b) = a/b*x" and
   11.26    rshift_nominator:        "(a::real) * b / c = a / c * b" and
   11.27  
   11.28    exp_pow:                 "(a \<up> b) \<up> c = a \<up> (b * c)" and
   11.29 @@ -178,9 +178,9 @@
   11.30    radd_0_right:            "k + 0 = (k::real)" and
   11.31  
   11.32    radd_real_const_eq:
   11.33 -          "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)" and
   11.34 +          "[| a is_num; c is_num; d is_num |] ==> a/d + c/d = (a+c)/(d::real)" and
   11.35    radd_real_const:
   11.36 -          "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"  
   11.37 +          "[| a is_num; b is_num; c is_num; d is_num |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"  
   11.38     and
   11.39  (*for AC-operators*)
   11.40    radd_commute:            "(m::real) + (n::real) = n + m" and
   11.41 @@ -375,7 +375,7 @@
   11.42  	     \<^rule_thm>\<open>and_commute\<close>,
   11.43  	     \<^rule_thm>\<open>or_commute\<close>,
   11.44      
   11.45 -	     \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
   11.46 +	     \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
   11.47  	     \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
   11.48      
   11.49  	     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
   11.50 @@ -416,7 +416,7 @@
   11.51  	     \<^rule_thm>\<open>root_ge0_1\<close>,
   11.52  	     \<^rule_thm>\<open>root_ge0_2\<close>,
   11.53      
   11.54 -	     \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
   11.55 +	     \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
   11.56  	     \<^rule_eval>\<open>contains_root\<close> (eval_contains_root "#eval_contains_root"),
   11.57  	     \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
   11.58  	     \<^rule_eval>\<open>contains_root\<close> (eval_contains_root"#contains_root_"),
   11.59 @@ -626,10 +626,10 @@
   11.60  	     \<^rule_thm_sym>\<open>real_mult_2\<close>,	 (*"z1 + z1 = 2 * z1"*)
   11.61  	     \<^rule_thm>\<open>real_mult_2_assoc\<close>,	 (*"z1 + (z1 + k) = 2 * z1 + k"*)
   11.62      
   11.63 -	     \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
   11.64 -	     \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) =  (l + m) * n + k"*)
   11.65 -	     \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_const ==> n + m * n = (1 + m) * n"*)
   11.66 -	     \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
   11.67 +	     \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
   11.68 +	     \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) =  (l + m) * n + k"*)
   11.69 +	     \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
   11.70 +	     \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
   11.71      
   11.72  	     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
   11.73  	     \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
   11.74 @@ -674,10 +674,10 @@
   11.75      	(*\<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)*)
   11.76      	\<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*)
   11.77      
   11.78 -    	\<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
   11.79 -    	\<^rule_thm>\<open>real_num_collect_assoc\<close>,	 (*"[| l is_const; m is_const |] ==>  l * n + (m * n + k) =  (l + m) * n + k"*)
   11.80 -    	\<^rule_thm>\<open>real_one_collect\<close>,	 (*"m is_const ==> n + m * n = (1 + m) * n"*)
   11.81 -    	\<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
   11.82 +    	\<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |] ==> l * n + m * n = (l + m) * n"*)
   11.83 +    	\<^rule_thm>\<open>real_num_collect_assoc\<close>,	 (*"[| l is_num; m is_num |] ==>  l * n + (m * n + k) =  (l + m) * n + k"*)
   11.84 +    	\<^rule_thm>\<open>real_one_collect\<close>,	 (*"m is_num ==> n + m * n = (1 + m) * n"*)
   11.85 +    	\<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
   11.86      
   11.87      	\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
   11.88      	\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),

    12.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Aug 18 11:35:24 2021 +0200
    12.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Aug 18 16:03:08 2021 +0200
    12.3 @@ -31,9 +31,6 @@
    12.4    abs              :: "real => real"            ("(|| _ ||)")
    12.5    (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
    12.6    absset           :: "real set => real"        ("(||| _ |||)")
    12.7 -  (*is numeral constant ?*)
    12.8 -  is_const        :: "real => bool"            ("_ is'_const" 10)
    12.9 -  (*is_const rename to is_num FIXXXME.WN.16.5.03 *)
   12.10    is_atom         :: "real => bool"            ("_ is'_atom" 10)
   12.11    is_num         :: "real => bool"             ("_ is'_num" 10)
   12.12    is_even         :: "real => bool"            ("_ is'_even" 10)
   12.13 @@ -315,15 +312,15 @@
   12.14      else NONE
   12.15    | eval_is_even _ _ _ _ = NONE; 
   12.16  
   12.17 -(*("is_const",("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"))*)
   12.18 -fun eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ Const ("Partial_Fractions.AA", _))) _ =
   12.19 +(*("is_num",("Prog_Expr.is_num", Prog_Expr.eval_is_num "#is_num_"))*)
   12.20 +fun eval_const thmid _ (t as (Const (\<^const_name>\<open>is_num\<close>, _) $ Const ("Partial_Fractions.AA", _))) _ =
   12.21      (*TODO get rid of this special case*)
   12.22      SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
   12.23        HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
   12.24 -  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ Const _)) _ =
   12.25 +  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_num\<close>, _) $ Const _)) _ =
   12.26      SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
   12.27        HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
   12.28 -  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ n)) _ =
   12.29 +  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_num\<close>, _) $ n)) _ =
   12.30  	   if TermC.is_num n
   12.31  	   then SOME (TermC.mk_thmid thmid (TermC.string_of_num n) "",
   12.32         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))