1.1 --- a/src/Tools/isac/Knowledge/Atools.thy	Thu Sep 23 12:56:51 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Atools.thy	Thu Sep 23 14:49:23 2010 +0200
     1.3 @@ -240,7 +240,7 @@
     1.4    | eval_const _ _ _ _ = NONE; 
     1.5  
     1.6  (*. evaluate binary, associative, commutative operators: *,+,^ .*)
     1.7 -(*("PLUS"    ,("op +"        ,eval_binop "#add_")),
     1.8 +(*("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
     1.9    ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
    1.10    ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))*)
    1.11  
    1.12 @@ -278,8 +278,8 @@
    1.13  	case (numeral t1, numeral t2) of
    1.14  	    (SOME n1, SOME n2) =>
    1.15  	    let val (T1,T2,Trange) = dest_binop_typ t0
    1.16 -		val res = calc (if op0 = "op -" then "op +" else op0) n1 n2
    1.17 -		(*WN071229 "HOL.divide" never tried*)
    1.18 +		val res = calc (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0) n1 n2
    1.19 +		(*WN071229 "Rings.inverse_class.divide" never tried*)
    1.20  		val rhs = var_op_float v op_ t0 T1 res
    1.21  		val prop = Trueprop $ (mk_equality (t, rhs))
    1.22  	    in SOME (mk_thmid_f thmid n1 n2, prop) end
    1.23 @@ -293,7 +293,7 @@
    1.24    if op0 = op0' then
    1.25  	case (numeral t1, numeral t2) of
    1.26  	    (SOME n1, SOME n2) =>
    1.27 -	    if op0 = "op -" then NONE else
    1.28 +	    if op0 = "Groups.minus_class.minus" then NONE else
    1.29  	    let val (T1,T2,Trange) = dest_binop_typ t0
    1.30  		val res = calc op0 n1 n2
    1.31  		val rhs = float_op_var v op_ t0 T1 res
    1.32 @@ -314,7 +314,7 @@
    1.33         | _ => NONE)
    1.34    | eval_binop _ _ _ _ = NONE; 
    1.35  (*
    1.36 -> val SOME (thmid, t) = eval_binop "#add_" "op +" (str2term "-1 + 2") thy;
    1.37 +> val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" (str2term "-1 + 2") thy;
    1.38  > term2str t;
    1.39  val it = "-1 + 2 = 1"
    1.40  > val t = str2term "-1 * (-1 * a)";
    1.41 @@ -449,8 +449,8 @@
    1.42  (** evaluation on the metalevel **)
    1.43  
    1.44  (*. evaluate HOL.divide .*)
    1.45 -(*("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_e"))*)
    1.46 -fun eval_cancel (thmid:string) "HOL.divide" (t as 
    1.47 +(*("DIVIDE" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e"))*)
    1.48 +fun eval_cancel (thmid:string) "Rings.inverse_class.divide" (t as 
    1.49  	       (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy = 
    1.50      (case (int_of_str n1, int_of_str n2) of
    1.51  	 (SOME n1', SOME n2') =>
    1.52 @@ -523,10 +523,10 @@
    1.53    | list2sum [s] = s
    1.54    | list2sum (s::ss) = 
    1.55      let fun sum su [s'] = 
    1.56 -	    Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
    1.57 +	    Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
    1.58  		  $ su $ s'
    1.59  	  | sum su (s'::ss') = 
    1.60 -	    sum (Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
    1.61 +	    sum (Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
    1.62  		  $ su $ s') ss'
    1.63      in sum s ss end;
    1.64  
    1.65 @@ -561,7 +561,7 @@
    1.66  val list_rls = 
    1.67      append_rls "list_rls" list_rls
    1.68  	       [Calc ("op *",eval_binop "#mult_"),
    1.69 -		Calc ("op +", eval_binop "#add_"), 
    1.70 +		Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
    1.71  		Calc ("op <",eval_equ "#less_"),
    1.72  		Calc ("op <=",eval_equ "#less_equal_"),
    1.73  		Calc ("Atools.ident",eval_ident "#ident_"),
    1.74 @@ -591,8 +591,8 @@
    1.75  		Calc ("op =",eval_equal "#equal_"),
    1.76  
    1.77  		Thm  ("real_unari_minus",num_str @{thm real_unari_minus}),
    1.78 -		Calc ("op +",eval_binop "#add_"),
    1.79 -		Calc ("op -",eval_binop "#sub_"),
    1.80 +		Calc ("Groups.plus_class.plus",eval_binop "#add_"),
    1.81 +		Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
    1.82  		Calc ("op *",eval_binop "#mult_")
    1.83  		];
    1.84  
    1.85 @@ -708,10 +708,10 @@
    1.86      ("leq"      ,("op <="       ,eval_equ "#less_equal_")),
    1.87      ("ident"    ,("Atools.ident",eval_ident "#ident_")),
    1.88      ("equal"    ,("op =",eval_equal "#equal_")),
    1.89 -    ("PLUS"     ,("op +"        ,eval_binop "#add_")),
    1.90 -    ("MINUS"    ,("op -",eval_binop "#sub_")),
    1.91 +    ("PLUS"     ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
    1.92 +    ("MINUS"    ,("Groups.minus_class.minus",eval_binop "#sub_")),
    1.93      ("TIMES"    ,("op *"        ,eval_binop "#mult_")),
    1.94 -    ("DIVIDE"  ,("HOL.divide"  ,eval_cancel "#divide_e")),
    1.95 +    ("DIVIDE"  ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),
    1.96      ("POWER"   ,("Atools.pow"  ,eval_binop "#power_")),
    1.97      ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum ""))
    1.98      ]);
    1.99 @@ -724,7 +724,7 @@
   1.100  				rew_ord = ("termlessI",termlessI), 
   1.101  				erls = e_rls, 
   1.102  				srls = Erls, calc = [], (*asm_thm = [],*)
   1.103 -				rules = [Calc ("op +", eval_binop "#add_"),
   1.104 +				rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"),
   1.105  					 Calc ("op <",eval_equ "#less_")
   1.106  					 (*    ~~~~~~ for nth_Cons_*)
   1.107  					 ],