1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Wed Aug 18 16:46:22 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Wed Aug 18 20:34:41 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   (* re-establish intermed.TOODOO *)
     1.8    val is_variable: term -> bool
     1.9    val is_bdv: string -> bool
    1.10    val is_bdv_subst: term -> bool

     2.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Wed Aug 18 16:46:22 2021 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Wed Aug 18 20:34:41 2021 +0200
     2.3 @@ -1319,12 +1319,8 @@
     2.4  
     2.5  ML \<open>@{term "1 is_num"}\<close> (*.."Prog_Expr.is_num" IS KNOWN TOODOO*)
     2.6  rule_set_knowledge
     2.7 -  norm_Poly = \<open>prep_rls' norm_Poly\<close> 
     2.8 -(*/---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------\*)
     2.9 -and
    2.10 -  Poly_erls = \<open>prep_rls' Poly_erls\<close> (*FIXXXME:del with rls.rls'*) 
    2.11 -(*\---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------/*)
    2.12 -and
    2.13 +  norm_Poly = \<open>prep_rls' norm_Poly\<close> and
    2.14 +  Poly_erls = \<open>prep_rls' Poly_erls\<close> and
    2.15    expand = \<open>prep_rls' expand\<close> and
    2.16    expand_poly = \<open>prep_rls' expand_poly\<close> and
    2.17    simplify_power = \<open>prep_rls' simplify_power\<close> and

     3.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy	Wed Aug 18 16:46:22 2021 +0200
     3.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy	Wed Aug 18 20:34:41 2021 +0200
     3.3 @@ -130,7 +130,7 @@
     3.4  val SEq $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 
     3.5  	"  ((Try (Repeat (Rewrite ''real_diff_minus''))) #>  \
     3.6          \   (Try (Repeat (Rewrite ''add.commute''))) #> \
     3.7 -        \   (Try (Repeat (Rewrite ''mult_commute'')))) t";
     3.8 +        \   (Try (Repeat (Rewrite ''mult_commute'')))) t"; (*has not yet been needed*)
     3.9  
    3.10  fun rule2stac _ (Rule.Thm (thmID, _)) = Try $ (Repeat $ (Rew $ HOLogic.mk_string thmID))
    3.11    | rule2stac thy (Rule.Eval (c, _)) = Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))
    3.12 @@ -213,7 +213,7 @@
    3.13  fun prep_rls _ Rule_Set.Empty = raise ERROR "prep_rls: not required for Erls"
    3.14    | prep_rls thy (Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) = 
    3.15        let
    3.16 -        val sc = (rules2scr_Rls thy rules)
    3.17 +        val sc = rules2scr_Rls thy rules
    3.18        in
    3.19          Rule_Def.Repeat {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
    3.20    	      calc = get_calcs thy sc,

     4.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Aug 18 16:46:22 2021 +0200
     4.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Aug 18 20:34:41 2021 +0200
     4.3 @@ -31,7 +31,6 @@
     4.4    abs              :: "real => real"            ("(|| _ ||)")
     4.5    (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
     4.6    absset           :: "real set => real"        ("(||| _ |||)")
     4.7 -  is_const        :: "real => bool"            ("_ is'_const" 10) (* re-establish intermed.TOODOO *)
     4.8    is_atom         :: "real => bool"            ("_ is'_atom" 10)
     4.9    is_num         :: "real => bool"             ("_ is'_num" 10)
    4.10    is_even         :: "real => bool"            ("_ is'_even" 10)
    4.11 @@ -70,7 +69,6 @@
    4.12      val eval_is_num: string -> string -> term -> 'a -> (string * term) option
    4.13      val even: int -> bool
    4.14      val eval_is_even: string -> string -> term -> 'a -> (string * term) option
    4.15 -    val eval_const: string -> string -> term -> 'a -> (string * term) option
    4.16      val eval_equ: string -> string -> term -> 'a -> (string * term) option
    4.17      val eval_ident: string -> string -> term -> theory -> (string * term) option
    4.18      val eval_equal: string -> string -> term -> theory -> (string * term) option
    4.19 @@ -313,22 +311,6 @@
    4.20      else NONE
    4.21    | eval_is_even _ _ _ _ = NONE; 
    4.22  
    4.23 -(*("is_const",("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"))*)
    4.24 -fun eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ Const ("Partial_Fractions.AA", _))) _ =
    4.25 -    (*TODO get rid of this special case*)
    4.26 -    SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
    4.27 -      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    4.28 -  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ Const _)) _ =
    4.29 -    SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
    4.30 -      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    4.31 -  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ n)) _ =
    4.32 -	   if TermC.is_num n
    4.33 -	   then SOME (TermC.mk_thmid thmid (TermC.string_of_num n) "",
    4.34 -       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    4.35 -	   else SOME (TermC.mk_thmid thmid (UnparseC.term n) "",
    4.36 -       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    4.37 -  | eval_const _ _ _ _ = NONE; 
    4.38 -
    4.39  (*. evaluate binary, associative, commutative operators: *,+,^ .*)
    4.40  (*("PLUS"    ,(\<^const_name>\<open>plus\<close>        , (**)eval_binop "#add_")),
    4.41    ("TIMES"   ,(\<^const_name>\<open>times\<close>        , (**)eval_binop "#mult_")),
    4.42 @@ -546,12 +528,17 @@
    4.43  
    4.44  rule_set_knowledge prog_expr = prog_expr
    4.45  
    4.46 +calculation lhs = \<open>Prog_Expr.eval_lhs ""\<close>
    4.47 +calculation rhs = \<open>Prog_Expr.eval_rhs ""\<close>
    4.48 +calculation Vars = \<open>Prog_Expr.eval_var "#Vars_"\<close>
    4.49  calculation matches = \<open>Prog_Expr.eval_matches "#matches_"\<close>
    4.50  calculation matchsub = \<open>Prog_Expr.eval_matchsub "#matchsub_"\<close>
    4.51 -calculation Vars = \<open>Prog_Expr.eval_var "#Vars_"\<close>
    4.52 -calculation lhs = \<open>Prog_Expr.eval_lhs ""\<close>
    4.53 -calculation rhs = \<open>Prog_Expr.eval_rhs ""\<close>
    4.54 -(*\\------------------------- from Tools .thy-------------------------------------------------//*)
    4.55 +
    4.56 +calculation some_occur_in = \<open>Prog_Expr.eval_some_occur_in "#some_occur_in_"\<close>
    4.57 +calculation occurs_in = \<open>Prog_Expr.eval_occurs_in "#occurs_in_"\<close>
    4.58 +calculation is_atom = \<open>Prog_Expr.eval_is_atom "#is_atom_"\<close>
    4.59 +calculation is_num = \<open>Prog_Expr.eval_is_num "#is_num_"\<close>
    4.60 +calculation is_even = \<open>Prog_Expr.eval_is_even "#is_even_"\<close>
    4.61  ML \<open>
    4.62  \<close> ML \<open>
    4.63  \<close> ML \<open>

     5.1 --- a/test/Tools/isac/BaseDefinitions/kestore.sml	Wed Aug 18 16:46:22 2021 +0200
     5.2 +++ b/test/Tools/isac/BaseDefinitions/kestore.sml	Wed Aug 18 20:34:41 2021 +0200
     5.3 @@ -1,6 +1,9 @@
     5.4 -(* Title: tests for Know_Store.thy
     5.5 +(* Title:  BaseDefinitions/kestore.sml
     5.6     Author: Walther Neuper
     5.7     Use is subject to license terms.
     5.8 +
     5.9 +theory Test_Some
    5.10 +  imports "Isac.Build_Isac" "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
    5.11  *)
    5.12  
    5.13  "-----------------------------------------------------------------------------";
    5.14 @@ -9,6 +12,7 @@
    5.15  "-----------------------------------------------------------------------------";
    5.16  "-------- fun check_kestore_rls ----------------------------------------------";
    5.17  "-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data ------------";
    5.18 +"-------- ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------";
    5.19  "-----------------------------------------------------------------------------";
    5.20  "-----------------------------------------------------------------------------";
    5.21  
    5.22 @@ -53,3 +57,44 @@
    5.23  
    5.24  (* add_rlss will take union_overwrite due to argument sequence *)
    5.25  
    5.26 +
    5.27 +"-------- ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------";
    5.28 +"-------- ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------";
    5.29 +"-------- ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------";
    5.30 +"~~~~~ fun prep_rls' , args:"; val (thy, (Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, rules, errpatts, ...})) =
    5.31 +  (@{theory}, Poly_erls);
    5.32 +
    5.33 +(*ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly*)
    5.34 +        val sc = 
    5.35 + Auto_Prog.rules2scr_Rls thy rules;
    5.36 +"~~~~~ fun rules2scr_Rls , args:"; val (thy, rules) = (thy, rules);
    5.37 +    (*if*) Auto_Prog.contain_bdv rules (*else*);
    5.38 +
    5.39 +(*+*)val t = Auto_Prog.rule2stac thy (nth 14 rules);
    5.40 +(*+*)UnparseC.term_in_thy @{theory} t;
    5.41 +
    5.42 +(*ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly*)
    5.43 + Auto_Prog.rule2stac thy (nth 17 rules);
    5.44 +"~~~~~ fun rule2stac , args:"; val (thy, (Rule.Eval (c, _))) = (thy, (nth 17 rules));
    5.45 +
    5.46 +(*+*)val Rule.Eval ("Prog_Expr.is_num", _) = nth 17 rules;
    5.47 +(*+*)c = "Prog_Expr.is_num";                                   (* <<<<<------------ is NOT found *)
    5.48 +
    5.49 +(*ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly*)
    5.50 +val "is_num" =
    5.51 +           assoc_calc thy c;
    5.52 +"~~~~~ fun assoc_calc , args:"; val (thy, calID) = (thy, c);
    5.53 +val calcs = 
    5.54 +       KEStore_Elems.get_calcs thy;
    5.55 +
    5.56 +(*+*)val ("is_polyrat_in", ("Poly.is_polyrat_in", _)) = nth 17 calcs; (* <<<<<------- is_atom <> is_num *)
    5.57 +(*+*)map fst calcs = (*..WITH declare [[ML_print_depth = 999]]*)
    5.58 +   ["Test.precond_rootmet", "contains_root", "Test.precond_rootpbl", "is_f_x", "primed", "is_normSqrtTerm_in", "is_rootTerm_in", "SQRT", "is_sqrtTerm_in", "is_ratequation_in", "is_rootRatAddTerm_in", "add_new_c",
    5.59 +    "occur_exactly_in", "is_addUnordered", "is_polyexp", "is_poly_in", "is_polyrat_in", "POWER", "TIMES", "PLUS", "ident", "le", "is_atom", "occurs_in", "is_num", "matchsub", "Vars", "lhs", "rhs", "matches",
    5.60 +    "some_occur_in", "is_even", "leq", "equal", "MINUS", "DIVIDE", "boollist2sum", "is_expanded_in", "has_degree_in", "is_multUnordered", "is_expanded"];
    5.61 +(*+*)map (fst o snd) calcs = (*..WITH declare [[ML_print_depth = 999]]*)
    5.62 +   ["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",
    5.63 +    "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",
    5.64 +    "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",
    5.65 +    "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",
    5.66 +    "Rings.divide_class.divide", "Prog_Expr.boollist2sum", "Poly.is_expanded_in", "Poly.has_degree_in", "Poly.is_multUnordered", "Rational.is_expanded"];

     6.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Wed Aug 18 16:46:22 2021 +0200
     6.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Wed Aug 18 20:34:41 2021 +0200
     6.3 @@ -255,8 +255,8 @@
     6.4  (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
     6.5  
     6.6  (*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
     6.7 -   ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
     6.8 -    "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
     6.9 +   ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
    6.10 +    "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
    6.11  (*this is new since ThmC.numerals_to_Free.-----\\*)
    6.12      "Calculate PLUS"]
    6.13    then () else error "specific_from_prog ([1], Res) 1 CHANGED";  (*GOON*)
    6.14 @@ -264,8 +264,8 @@
    6.15  
    6.16  (*+*)if map Tactic.input_to_string (specific_from_prog pt p) = [
    6.17    "Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")",
    6.18 -  "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
    6.19 -  "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
    6.20 +  "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
    6.21 +  "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
    6.22    (*this is new since ThmC.numerals_to_Free.-----\\*)
    6.23    "Calculate PLUS",
    6.24    (*this is new since ThmC.numerals_to_Free.-----//*)

     7.1 --- a/test/Tools/isac/Knowledge/diff.sml	Wed Aug 18 16:46:22 2021 +0200
     7.2 +++ b/test/Tools/isac/Knowledge/diff.sml	Wed Aug 18 20:34:41 2021 +0200
     7.3 @@ -52,10 +52,10 @@
     7.4    SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
     7.5  | _ => error "rewrite_set_  Not (x =!= a)  changed";
     7.6  
     7.7 -val t =(Thm.term_of o the o (TermC.parse thy)) "2 is_const";
     7.8 +val t =(Thm.term_of o the o (TermC.parse thy)) "2 is_num";
     7.9  case rewrite_set_ thy false erls_diff t of
    7.10    SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
    7.11 -| _ => error "rewrite_set_   2 is_const   changed";
    7.12 +| _ => error "rewrite_set_   2 is_num   changed";
    7.13  
    7.14  val thm = @{thm diff_const};
    7.15  val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x x";

     8.1 --- a/test/Tools/isac/Knowledge/rational-old.sml	Wed Aug 18 16:46:22 2021 +0200
     8.2 +++ b/test/Tools/isac/Knowledge/rational-old.sml	Wed Aug 18 20:34:41 2021 +0200
     8.3 @@ -708,7 +708,7 @@
     8.4  !    Thm ("sym_#add_(-3)_3", "0 = (-3) + 3"),
     8.5   
     8.6  ?    Thm ("sym_real_num_collect_assoc",
     8.7 -       "[| ?l is_const; ?m is_const |]
     8.8 +       "[| ?l is_num; ?m is_num |]
     8.9    	==> (?l + ?m) * ?n + ?k = ?l * ?n + (?m * ?n + ?k)"),
    8.10  OK   Thm ("sym_real_mult_2_assoc", "2 * ?z1.0 + ?k = ?z1.0 + (?z1.0 + ?k)"),
    8.11  OK   Thm ("sym_real_add_left_commute", "?y + (?x + ?z) = ?x + (?y + ?z)"),

     9.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml	Wed Aug 18 16:46:22 2021 +0200
     9.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Wed Aug 18 20:34:41 2021 +0200
     9.3 @@ -121,7 +121,7 @@
     9.4  
     9.5  val given  = ["equation (l=(0::real))",
     9.6  	     "bound_variable bdv"];
     9.7 -val where_ = ["l is_linear_in bdv", "bdv is_const"];
     9.8 +val where_ = ["l is_linear_in bdv", "bdv is_atom"];
     9.9  val find   = ["l::real"];
    9.10  val with_  = ["l = (%x. l) bdv"];
    9.11  val chkpbl = map (the o (parseold thy)) (given @ where_ @ find @ with_);

    10.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Wed Aug 18 16:46:22 2021 +0200
    10.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Wed Aug 18 20:34:41 2021 +0200
    10.3 @@ -19,7 +19,7 @@
    10.4  "----------- fun cancel_int --------------------------------------------------------------------";
    10.5  "----------- RE-BUILD fun calcul ---------------------------------------------------------------";
    10.6  "----------- get_pair with 3 args -----------------------";
    10.7 -"----------- calculate (2 * x is_const) -----------------";
    10.8 +"----------- calculate (2 * x is_num) -------------------";
    10.9  "----------- fun get_pair: examples ------------------------------------------------------------";
   10.10  "----------- fun adhoc_thm: examples -----------------------------------------------------------";
   10.11  "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
   10.12 @@ -135,15 +135,14 @@
   10.13   val (t,_) = the (rewrite_set_ thy false rls t);
   10.14  (*val t = Free ("3", "Real.real") : term*)
   10.15  
   10.16 -(*--------------(3): is_const works ?: -------------------------------------*)
   10.17 - val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_const";
   10.18 +(*--------------(3): is_num works ?: -------------------------------------*)
   10.19 + val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_num";
   10.20   TermC.atomty t;
   10.21   rewrite_set_ @{theory Test} false tval_rls t;
   10.22  (*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*)
   10.23  
   10.24 - val t = TermC.str2term "2 * x is_const";
   10.25 - val SOME (str,t') = eval_const "" "" t (@{theory "Isac_Knowledge"});
   10.26 - UnparseC.term t';
   10.27 + val t = TermC.str2term "2 * x is_num";
   10.28 + val NONE = eval_is_num "" "" t (@{theory "Isac_Knowledge"});
   10.29   
   10.30  
   10.31  "----------- check calculate bottom up ------------------";
   10.32 @@ -352,17 +351,18 @@
   10.33  then () else error "evaluate.sml get_pair with 3 args:occur_exactly_in";
   10.34  
   10.35  
   10.36 -"----------- calculate (2 * x is_const) -----------------";
   10.37 -"----------- calculate (2 * x is_const) -----------------";
   10.38 -"----------- calculate (2 * x is_const) -----------------";
   10.39 -val t = TermC.str2term "2 * x is_const";
   10.40 -val SOME (str, t') = eval_const "" "" t @{theory Test};
   10.41 -if UnparseC.term t' = "(2 * x is_const) = False" then ()
   10.42 -else error "eval_const 2 * x is_const CHANGED";
   10.43 +"----------- calculate (2 * x is_num) -------------------";
   10.44 +"----------- calculate (2 * x is_num) -------------------";
   10.45 +"----------- calculate (2 * x is_num) -------------------";
   10.46 +val t = TermC.str2term "(2::real) * x is_num";
   10.47 +
   10.48 +val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t @{theory Test};
   10.49 +if UnparseC.term t' = "(2 * x is_num) = False" then ()
   10.50 +else error "is_num 2 * x is_num CHANGED";
   10.51  
   10.52  val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t;
   10.53  if UnparseC.term t' = "False" then ()
   10.54 -else error "rewrite_set_ 2 * x is_const CHANGED";
   10.55 +else error "rewrite_set_ 2 * x is_num CHANGED";
   10.56  
   10.57  "----------- fun get_pair: examples ------------------------------------------------------------";
   10.58  "----------- fun get_pair: examples ------------------------------------------------------------";
   10.59 @@ -409,11 +409,11 @@
   10.60  "----------- fun adhoc_thm: examples -----------------------------------------------------------";
   10.61  "----------- fun adhoc_thm: examples -----------------------------------------------------------";
   10.62  (*--------------------------------------------------------------------vvvvvvvvvv*)
   10.63 -val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_const");
   10.64 -val t = @{term "9 is_const"};
   10.65 +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_num");
   10.66 +val t = @{term "9 is_num"};
   10.67  val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
   10.68 -if str = "#is_const_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_const) = True"
   10.69 -then () else error "adhoc_thm  9 is_const  changed";
   10.70 +if str = "#is_num_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_num) = True"
   10.71 +then () else error "adhoc_thm  9 is_num  changed";
   10.72  
   10.73  case assoc_calc thy \<^const_name>\<open>less\<close> of
   10.74    "le" => () | _ => error "Orderings.ord_class.less <-> le changed";

    11.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml	Wed Aug 18 16:46:22 2021 +0200
    11.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml	Wed Aug 18 20:34:41 2021 +0200
    11.3 @@ -9,7 +9,7 @@
    11.4  "-----------------------------------------------------------------------------------------------";
    11.5  "-------- fun eval_is_atom ---------------------------------------------------------------------";
    11.6  "-------- fun eval_is_even ---------------------------------------------------------------------";
    11.7 -"-------- fun eval_const -----------------------------------------------------------------------";
    11.8 +"-------- fun eval_is_num ----------------------------------------------------------------------";
    11.9  "-------- fun eval_cancel ----------------------------------------------------------------------";
   11.10  "-------- fun eval_equ -------------------------------------------------------------------------";
   11.11  "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
   11.12 @@ -86,38 +86,38 @@
   11.13  | NONE => ();
   11.14  
   11.15  
   11.16 -"-------- fun eval_const -----------------------------------------------------------------------";
   11.17 -"-------- fun eval_const -----------------------------------------------------------------------";
   11.18 -"-------- fun eval_const -----------------------------------------------------------------------";
   11.19 -val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_const";
   11.20 +"-------- fun eval_is_num ----------------------------------------------------------------------";
   11.21 +"-------- fun eval_is_num ----------------------------------------------------------------------";
   11.22 +"-------- fun eval_is_num ----------------------------------------------------------------------";
   11.23 +val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_num";
   11.24  case rewrite_set_ @{theory Test} false tval_rls t of
   11.25    SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
   11.26 -| _ => error "2 is_const CHANGED";
   11.27 +| _ => error "2 is_num CHANGED";
   11.28  
   11.29 -val t = TermC.str2term "2 * x is_const";
   11.30 -val SOME (str, t') = eval_const "" "" t (@{theory "Isac_Knowledge"});
   11.31 -if UnparseC.term t' = "(2 * x is_const) = False" then ()
   11.32 -else error "(2 * x is_const) = False CHANGED";
   11.33 +val t = TermC.str2term "2 * x is_num";
   11.34 +val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
   11.35 +if UnparseC.term t' = "(2 * x is_num) = False" then ()
   11.36 +else error "(2 * x is_num) = False CHANGED";
   11.37  
   11.38 -val t = TermC.str2term "- 2 is_const";
   11.39 -val SOME (str, t') = eval_const "" "" t (@{theory "Isac_Knowledge"});
   11.40 -if UnparseC.term t' = "(- 2 is_const) = True" then ()
   11.41 -else error "(- 2 is_const) = False CHANGED";
   11.42 +val t = TermC.str2term "- 2 is_num";
   11.43 +val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
   11.44 +if UnparseC.term t' = "(- 2 is_num) = True" then ()
   11.45 +else error "(- 2 is_num) = False CHANGED";
   11.46  
   11.47 -val t = TermC.str2term "- 1 is_const";
   11.48 -val SOME (str, t') = eval_const "" "" t (@{theory "Isac_Knowledge"});
   11.49 -if UnparseC.term t' = "(- 1 is_const) = True" then ()
   11.50 -else error "(- 1 is_const) = False CHANGED";
   11.51 +val t = TermC.str2term "- 1 is_num";
   11.52 +val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
   11.53 +if UnparseC.term t' = "(- 1 is_num) = True" then ()
   11.54 +else error "(- 1 is_num) = False CHANGED";
   11.55  
   11.56 -val t = TermC.str2term "0 is_const";
   11.57 -val SOME (str, t') = eval_const "" "" t (@{theory "Isac_Knowledge"});
   11.58 -if UnparseC.term t' = "(0 is_const) = True" then ()
   11.59 -else error "(0 is_const) = False CHANGED";
   11.60 +val t = TermC.str2term "0 is_num";
   11.61 +val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
   11.62 +if UnparseC.term t' = "(0 is_num) = True" then ()
   11.63 +else error "(0 is_num) = False CHANGED";
   11.64  
   11.65 -val t = TermC.str2term "AA is_const";
   11.66 -val SOME (str, t') = eval_const "" "" t (@{theory "Isac_Knowledge"});
   11.67 -if UnparseC.term t' = "(AA is_const) = False" then ()
   11.68 -else error "(0 is_const) = False CHANGED";
   11.69 +val t = TermC.str2term "AA is_num";
   11.70 +val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
   11.71 +if UnparseC.term t' = "(AA is_num) = False" then ()
   11.72 +else error "(0 is_num) = False CHANGED";
   11.73  
   11.74  
   11.75  "-------- fun eval_cancel ----------------------------------------------------------------------";

    12.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Wed Aug 18 16:46:22 2021 +0200
    12.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Wed Aug 18 20:34:41 2021 +0200
    12.3 @@ -51,6 +51,7 @@
    12.4       Also backup files (#* ) recognised by jEdit cause this trouble                    *)
    12.5  (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
    12.6  (** )"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Thy_All"( *TODOO*)
    12.7 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
    12.8  (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt"
    12.9  (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test"
   12.10  (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt"

    13.1 --- a/test/Tools/isac/Test_Some.thy	Wed Aug 18 16:46:22 2021 +0200
    13.2 +++ b/test/Tools/isac/Test_Some.thy	Wed Aug 18 20:34:41 2021 +0200
    13.3 @@ -1,5 +1,5 @@
    13.4  theory Test_Some
    13.5 -  imports "Isac.Build_Isac"
    13.6 +  imports "Isac.Build_Isac" "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
    13.7  begin 
    13.8  
    13.9  ML \<open>open ML_System\<close>
   13.10 @@ -104,8 +104,15 @@
   13.11  \<close> ML \<open>
   13.12  \<close>
   13.13  
   13.14 +section \<open>===================================================================================\<close>
   13.15 +ML \<open>
   13.16 +\<close> ML \<open>
   13.17 +\<close> ML \<open>
   13.18 +\<close> ML \<open>
   13.19 +\<close>
   13.20 +
   13.21  (*ML_file "MathEngBasic/rewrite.sml"   TOODOO.1 loops with real_unary_minus *)
   13.22 -section \<open>===================================================================================\<close>
   13.23 +section \<open>======== check test/../rewrite.sml ===============================================\<close>
   13.24  ML \<open>
   13.25  \<close> ML \<open>
   13.26  (* Title: "MathEngBasic/rewrite.sml"