1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Fri Jan 17 12:37:21 2020 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Fri Jan 17 13:14:11 2020 +0100
     1.3 @@ -58,7 +58,7 @@
     1.4  ML \<open>
     1.5  \<close> ML \<open>
     1.6  val Atools_erls = Rule.append_rls "Atools_erls" Rule.e_rls
     1.7 -  [ Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
     1.8 +  [ Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
     1.9      Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
    1.10  		(*"(~ True) = False"*)
    1.11  		Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
    1.12 @@ -79,18 +79,18 @@
    1.13  		Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
    1.14  		Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
    1.15  		
    1.16 -		Rule.Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
    1.17 -		Rule.Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
    1.18 +		Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
    1.19 +		Rule.Num_Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
    1.20  		
    1.21 -		Rule.Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),    
    1.22 -		Rule.Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
    1.23 -		Rule.Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),    
    1.24 -		Rule.Calc ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
    1.25 +		Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),    
    1.26 +		Rule.Num_Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
    1.27 +		Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),    
    1.28 +		Rule.Num_Calc ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
    1.29  \<close>
    1.30  
    1.31  ML \<open>
    1.32  val Atools_crls = Rule.append_rls "Atools_crls" Rule.e_rls
    1.33 -  [ Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
    1.34 +  [ Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
    1.35      Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
    1.36  		Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
    1.37  		Rule.Thm ("and_true", TermC.num_str @{thm and_true}),
    1.38 @@ -105,27 +105,27 @@
    1.39  		Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
    1.40  		Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
    1.41  		
    1.42 -		Rule.Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
    1.43 -		Rule.Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
    1.44 +		Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
    1.45 +		Rule.Num_Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
    1.46  		
    1.47 -		Rule.Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),    
    1.48 -		Rule.Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
    1.49 -		Rule.Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),    
    1.50 -		Rule.Calc ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
    1.51 +		Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),    
    1.52 +		Rule.Num_Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
    1.53 +		Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),    
    1.54 +		Rule.Num_Calc ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
    1.55  \<close>
    1.56  
    1.57  subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>
    1.58  text \<open>requires "eval_binop" from above\<close>
    1.59  ML \<open>
    1.60  val list_rls = Rule.append_rls "list_rls" list_rls
    1.61 -	[ Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
    1.62 -		Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), 
    1.63 -		Rule.Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
    1.64 -		Rule.Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
    1.65 -		Rule.Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
    1.66 -		Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),(*atom <> atom -> False*)
    1.67 +	[ Rule.Num_Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
    1.68 +		Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), 
    1.69 +		Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
    1.70 +		Rule.Num_Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
    1.71 +		Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
    1.72 +		Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),(*atom <> atom -> False*)
    1.73         
    1.74 -		Rule.Calc ("Prog_Expr.Vars",Prog_Expr.eval_var "#Vars_"),
    1.75 +		Rule.Num_Calc ("Prog_Expr.Vars",Prog_Expr.eval_var "#Vars_"),
    1.76  		
    1.77  		Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
    1.78  		Rule.Thm ("if_False",TermC.num_str @{thm if_False})];
    1.79 @@ -134,8 +134,8 @@
    1.80  	(Rule.Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
    1.81      erls = Rule.Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), 
    1.82      erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
    1.83 -    rules = [Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
    1.84 -      Rule.Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")
    1.85 +    rules = [Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
    1.86 +      Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")
    1.87        (*    ~~~~~~ for nth_Cons_*)],
    1.88      scr = Rule.EmptyScr},
    1.89      srls = Rule.Erls, calc = [], errpatts = [],