updated "op +", "op -", "op *". "HOL.divide" in src & test
find . -type f -exec sed -i s/"\"op +\""/"\"Groups.plus_class.plus\""/g {} \;
find . -type f -exec sed -i s/"\"op -\""/"\"Groups.minus_class.minus\""/g {} \;
find . -type f -exec sed -i s/"\"op *\""/"\"Groups.times_class.times\""/g {} \;
find . -type f -exec sed -i s/"\"HOL.divide\""/"\"Rings.inverse_class.divide\""/g {} \;
1.1 --- a/src/Tools/isac/Interpret/solve.sml Thu Sep 23 12:56:51 2010 +0200
1.2 +++ b/src/Tools/isac/Interpret/solve.sml Thu Sep 23 14:49:23 2010 +0200
1.3 @@ -91,7 +91,7 @@
1.4
1.5 (*13.9.02--------------
1.6 type ctr = (loc * pos) list;
1.7 -val ops = [("PLUS","op +"),("MINUS","op -"),("TIMES","op *"),
1.8 +val ops = [("PLUS","Groups.plus_class.plus"),("MINUS","Groups.minus_class.minus"),("TIMES","op *"),
1.9 ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")];
1.10 ML {*
1.11 @{term "PLUS"}; (*Free ("PLUS", "'a") : term*)
2.1 --- a/src/Tools/isac/Knowledge/Atools.thy Thu Sep 23 12:56:51 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Thu Sep 23 14:49:23 2010 +0200
2.3 @@ -240,7 +240,7 @@
2.4 | eval_const _ _ _ _ = NONE;
2.5
2.6 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
2.7 -(*("PLUS" ,("op +" ,eval_binop "#add_")),
2.8 +(*("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
2.9 ("TIMES" ,("op *" ,eval_binop "#mult_")),
2.10 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))*)
2.11
2.12 @@ -278,8 +278,8 @@
2.13 case (numeral t1, numeral t2) of
2.14 (SOME n1, SOME n2) =>
2.15 let val (T1,T2,Trange) = dest_binop_typ t0
2.16 - val res = calc (if op0 = "op -" then "op +" else op0) n1 n2
2.17 - (*WN071229 "HOL.divide" never tried*)
2.18 + val res = calc (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0) n1 n2
2.19 + (*WN071229 "Rings.inverse_class.divide" never tried*)
2.20 val rhs = var_op_float v op_ t0 T1 res
2.21 val prop = Trueprop $ (mk_equality (t, rhs))
2.22 in SOME (mk_thmid_f thmid n1 n2, prop) end
2.23 @@ -293,7 +293,7 @@
2.24 if op0 = op0' then
2.25 case (numeral t1, numeral t2) of
2.26 (SOME n1, SOME n2) =>
2.27 - if op0 = "op -" then NONE else
2.28 + if op0 = "Groups.minus_class.minus" then NONE else
2.29 let val (T1,T2,Trange) = dest_binop_typ t0
2.30 val res = calc op0 n1 n2
2.31 val rhs = float_op_var v op_ t0 T1 res
2.32 @@ -314,7 +314,7 @@
2.33 | _ => NONE)
2.34 | eval_binop _ _ _ _ = NONE;
2.35 (*
2.36 -> val SOME (thmid, t) = eval_binop "#add_" "op +" (str2term "-1 + 2") thy;
2.37 +> val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" (str2term "-1 + 2") thy;
2.38 > term2str t;
2.39 val it = "-1 + 2 = 1"
2.40 > val t = str2term "-1 * (-1 * a)";
2.41 @@ -449,8 +449,8 @@
2.42 (** evaluation on the metalevel **)
2.43
2.44 (*. evaluate HOL.divide .*)
2.45 -(*("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_e"))*)
2.46 -fun eval_cancel (thmid:string) "HOL.divide" (t as
2.47 +(*("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e"))*)
2.48 +fun eval_cancel (thmid:string) "Rings.inverse_class.divide" (t as
2.49 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
2.50 (case (int_of_str n1, int_of_str n2) of
2.51 (SOME n1', SOME n2') =>
2.52 @@ -523,10 +523,10 @@
2.53 | list2sum [s] = s
2.54 | list2sum (s::ss) =
2.55 let fun sum su [s'] =
2.56 - Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2.57 + Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2.58 $ su $ s'
2.59 | sum su (s'::ss') =
2.60 - sum (Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2.61 + sum (Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2.62 $ su $ s') ss'
2.63 in sum s ss end;
2.64
2.65 @@ -561,7 +561,7 @@
2.66 val list_rls =
2.67 append_rls "list_rls" list_rls
2.68 [Calc ("op *",eval_binop "#mult_"),
2.69 - Calc ("op +", eval_binop "#add_"),
2.70 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
2.71 Calc ("op <",eval_equ "#less_"),
2.72 Calc ("op <=",eval_equ "#less_equal_"),
2.73 Calc ("Atools.ident",eval_ident "#ident_"),
2.74 @@ -591,8 +591,8 @@
2.75 Calc ("op =",eval_equal "#equal_"),
2.76
2.77 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
2.78 - Calc ("op +",eval_binop "#add_"),
2.79 - Calc ("op -",eval_binop "#sub_"),
2.80 + Calc ("Groups.plus_class.plus",eval_binop "#add_"),
2.81 + Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
2.82 Calc ("op *",eval_binop "#mult_")
2.83 ];
2.84
2.85 @@ -708,10 +708,10 @@
2.86 ("leq" ,("op <=" ,eval_equ "#less_equal_")),
2.87 ("ident" ,("Atools.ident",eval_ident "#ident_")),
2.88 ("equal" ,("op =",eval_equal "#equal_")),
2.89 - ("PLUS" ,("op +" ,eval_binop "#add_")),
2.90 - ("MINUS" ,("op -",eval_binop "#sub_")),
2.91 + ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
2.92 + ("MINUS" ,("Groups.minus_class.minus",eval_binop "#sub_")),
2.93 ("TIMES" ,("op *" ,eval_binop "#mult_")),
2.94 - ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_e")),
2.95 + ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
2.96 ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
2.97 ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum ""))
2.98 ]);
2.99 @@ -724,7 +724,7 @@
2.100 rew_ord = ("termlessI",termlessI),
2.101 erls = e_rls,
2.102 srls = Erls, calc = [], (*asm_thm = [],*)
2.103 - rules = [Calc ("op +", eval_binop "#add_"),
2.104 + rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"),
2.105 Calc ("op <",eval_equ "#less_")
2.106 (* ~~~~~~ for nth_Cons_*)
2.107 ],
3.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Thu Sep 23 12:56:51 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Thu Sep 23 14:49:23 2010 +0200
3.3 @@ -185,11 +185,11 @@
3.4 [(*for asm in NTH_CONS ...*)
3.5 Calc ("op <",eval_equ "#less_"),
3.6 (*2nd NTH_CONS pushes n+-1 into asms*)
3.7 - Calc("op +", eval_binop "#add_")
3.8 + Calc("Groups.plus_class.plus", eval_binop "#add_")
3.9 ],
3.10 srls = Erls, calc = [],
3.11 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
3.12 - Calc("op +", eval_binop "#add_"),
3.13 + Calc("Groups.plus_class.plus", eval_binop "#add_"),
3.14 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
3.15 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
3.16 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
3.17 @@ -206,11 +206,11 @@
3.18 [(*for asm in NTH_CONS ...*)
3.19 Calc ("op <",eval_equ "#less_"),
3.20 (*2nd NTH_CONS pushes n+-1 into asms*)
3.21 - Calc("op +", eval_binop "#add_")
3.22 + Calc("Groups.plus_class.plus", eval_binop "#add_")
3.23 ],
3.24 srls = Erls, calc = [],
3.25 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
3.26 - Calc("op +", eval_binop "#add_"),
3.27 + Calc("Groups.plus_class.plus", eval_binop "#add_"),
3.28 Thm ("NTH_NIL", num_str @{thm NTH_NIL}),
3.29 Calc("Tools.lhs", eval_lhs "eval_lhs_"),
3.30 Calc("Atools.filter'_sameFunId",
4.1 --- a/src/Tools/isac/Knowledge/Delete.thy Thu Sep 23 12:56:51 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Delete.thy Thu Sep 23 14:49:23 2010 +0200
4.3 @@ -19,15 +19,15 @@
4.4
4.5 (*.used for calculating built in binary operations in Isabelle2002.
4.6 integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0)*)
4.7 -fun calc "op +" ((a, b), _:int * int) ((c, d), _:int * int) = (*FIXME.WN1008 drop Float.calc, var_op_float, float_op_var, term_of_float*)
4.8 +fun calc "Groups.plus_class.plus" ((a, b), _:int * int) ((c, d), _:int * int) = (*FIXME.WN1008 drop Float.calc, var_op_float, float_op_var, term_of_float*)
4.9 if b < d
4.10 then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*)
4.11 else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)
4.12 - | calc "op -" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
4.13 + | calc "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
4.14 ((a - c,0),(0,0))
4.15 | calc "op *" ((a, b), _) ((c, d), _) = (*FIXXXME precision*)
4.16 ((a * c, b + d), (0, 0))
4.17 - | calc "HOL.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
4.18 + | calc "Rings.inverse_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
4.19 ((a div c, 0), (0, 0))
4.20 | calc "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*)
4.21 ((power a c, 0), (0, 0))
4.22 @@ -37,7 +37,7 @@
4.23 (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^
4.24 (string_of_int c )^","^(string_of_int d )^"), ("^
4.25 (string_of_int p21)^","^(string_of_int p22)^"))");
4.26 -(*> calc "op +" ((~1,0),(0,0)) ((2,0),(0,0));
4.27 +(*> calc "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0));
4.28 val it = ((1,0),(0,0))*)
4.29
4.30 (*.convert internal floatingpoint prepresentation to int and float.*)
4.31 @@ -76,9 +76,9 @@
4.32 (Free (str_of_int p2, T)))))
4.33 end;
4.34 (*> val t = str2term "a + b";
4.35 -> val Const ("op +", optype) $ _ $ _ = t;
4.36 +> val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
4.37 > val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v";
4.38 -> t = var_op_float v "op +" optype HOLogic.realT ((11,~1),(0,0));
4.39 +> t = var_op_float v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));
4.40 val it = true : bool*)
4.41
4.42 (*.assoc. convert internal floatingpoint prepresentation to int and float.*)
4.43 @@ -94,9 +94,9 @@
4.44 (Free (str_of_int p2, T))))) $ v
4.45 end;
4.46 (*> val t = str2term "a + b";
4.47 -> val Const ("op +", optype) $ _ $ _ = t;
4.48 +> val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
4.49 > val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v";
4.50 -> t = float_op_var v "op +" optype HOLogic.realT ((11,~1),(0,0));
4.51 +> t = float_op_var v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));
4.52 val it = true : bool*)
4.53 *}
4.54
5.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Thu Sep 23 12:56:51 2010 +0200
5.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Thu Sep 23 14:49:23 2010 +0200
5.3 @@ -274,7 +274,7 @@
5.4 (*Rls_ discard_parentheses *3**),
5.5 Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
5.6 Rls_ separate_bdv2,
5.7 - Calc ("HOL.divide" ,eval_cancel "#divide_e")
5.8 + Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e")
5.9 ],
5.10 scr = EmptyScr}:rls;
5.11 *}
5.12 @@ -292,7 +292,7 @@
5.13 Rls_ discard_parentheses,
5.14 Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
5.15 Rls_ separate_bdv2,
5.16 - Calc ("HOL.divide" ,eval_cancel "#divide_e")
5.17 + Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e")
5.18 ],
5.19 scr = EmptyScr}:rls;
5.20 (*
5.21 @@ -362,14 +362,14 @@
5.22 erls = Erls, srls = Erls, calc = [],
5.23 rules = [(*for precond NTH_CONS ...*)
5.24 Calc ("op <",eval_equ "#less_"),
5.25 - Calc ("op +", eval_binop "#add_")
5.26 + Calc ("Groups.plus_class.plus", eval_binop "#add_")
5.27 (*immediately repeated rewrite pushes
5.28 '+' into precondition !*)
5.29 ],
5.30 scr = EmptyScr},
5.31 srls = Erls, calc = [],
5.32 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
5.33 - Calc ("op +", eval_binop "#add_"),
5.34 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
5.35 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
5.36 Thm ("tl_Cons",num_str @{thm tl_Cons}),
5.37 Thm ("tl_Nil",num_str @{thm tl_Nil}),
5.38 @@ -391,14 +391,14 @@
5.39 erls = Erls, srls = Erls, calc = [],
5.40 rules = [(*for precond NTH_CONS ...*)
5.41 Calc ("op <",eval_equ "#less_"),
5.42 - Calc ("op +", eval_binop "#add_")
5.43 + Calc ("Groups.plus_class.plus", eval_binop "#add_")
5.44 (*immediately repeated rewrite pushes
5.45 '+' into precondition !*)
5.46 ],
5.47 scr = EmptyScr},
5.48 srls = Erls, calc = [],
5.49 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
5.50 - Calc ("op +", eval_binop "#add_"),
5.51 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
5.52 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
5.53 Thm ("tl_Cons",num_str @{thm tl_Cons}),
5.54 Thm ("tl_Nil",num_str @{thm tl_Nil}),
5.55 @@ -458,7 +458,7 @@
5.56 append_rls "prls_2x2_linear_system" e_rls
5.57 [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
5.58 Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
5.59 - Calc ("op +", eval_binop "#add_"),
5.60 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
5.61 Calc ("op =",eval_equal "#equal_")
5.62 ],
5.63 SOME "solveSystem e_s v_s",
5.64 @@ -497,7 +497,7 @@
5.65 append_rls "prls_3x3_linear_system" e_rls
5.66 [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
5.67 Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
5.68 - Calc ("op +", eval_binop "#add_"),
5.69 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
5.70 Calc ("op =",eval_equal "#equal_")
5.71 ],
5.72 SOME "solveSystem e_s v_s",
5.73 @@ -513,7 +513,7 @@
5.74 append_rls "prls_4x4_linear_system" e_rls
5.75 [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
5.76 Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
5.77 - Calc ("op +", eval_binop "#add_"),
5.78 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
5.79 Calc ("op =",eval_equal "#equal_")
5.80 ],
5.81 SOME "solveSystem e_s v_s",
5.82 @@ -672,11 +672,11 @@
5.83 [(*for asm in NTH_CONS ...*)
5.84 Calc ("op <",eval_equ "#less_"),
5.85 (*2nd NTH_CONS pushes n+-1 into asms*)
5.86 - Calc("op +", eval_binop "#add_")
5.87 + Calc("Groups.plus_class.plus", eval_binop "#add_")
5.88 ],
5.89 srls = Erls, calc = [],
5.90 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
5.91 - Calc("op +", eval_binop "#add_"),
5.92 + Calc("Groups.plus_class.plus", eval_binop "#add_"),
5.93 Thm ("NTH_NIL",num_str @{thm NTH_NIL})],
5.94 scr = EmptyScr};
5.95 store_met
6.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Thu Sep 23 12:56:51 2010 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Thu Sep 23 14:49:23 2010 +0200
6.3 @@ -140,7 +140,7 @@
6.4 Thm ("integral_add",num_str @{thm integral_add}),
6.5 Thm ("integral_mult",num_str @{thm integral_mult}),
6.6 Thm ("integral_pow",num_str @{thm integral_pow}),
6.7 - Calc ("op +", eval_binop "#add_")(*for n+1*)
6.8 + Calc ("Groups.plus_class.plus", eval_binop "#add_")(*for n+1*)
6.9 ],
6.10 scr = EmptyScr};
6.11 *}
6.12 @@ -200,7 +200,7 @@
6.13 Thm ("divide_divide_eq_left",
6.14 num_str @{thm divide_divide_eq_left}),
6.15 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
6.16 - Calc ("HOL.divide" ,eval_cancel "#divide_e"),
6.17 + Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"),
6.18
6.19 Thm ("rat_power", num_str @{thm rat_power})
6.20 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
6.21 @@ -264,7 +264,7 @@
6.22 Rls_ discard_parentheses,
6.23 (*Rls_ collect_bdv, from make_polynomial_in*)
6.24 Rls_ separate_bdv2,
6.25 - Calc ("HOL.divide" ,eval_cancel "#divide_e")
6.26 + Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e")
6.27 ],
6.28 scr = EmptyScr}:rls;
6.29
6.30 @@ -302,7 +302,7 @@
6.31 * num_str @{thm add_divide_distrib})
6.32 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
6.33 * ]),
6.34 -* Calc ("HOL.divide" ,eval_cancel "#divide_e")
6.35 +* Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e")
6.36 * ],
6.37 * scr = EmptyScr
6.38 * }:rls);
7.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Thu Sep 23 12:56:51 2010 +0200
7.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Thu Sep 23 14:49:23 2010 +0200
7.3 @@ -55,7 +55,7 @@
7.4 [Thm ("real_assoc_1",num_str @{thm real_assoc_1})
7.5 (*
7.6 Don't use
7.7 - Calc ("HOL.divide", eval_cancel "#divide_e"),
7.8 + Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
7.9 Calc ("Atools.pow" ,eval_binop "#power_"),
7.10 *)
7.11 ];
7.12 @@ -66,7 +66,7 @@
7.13 [Thm ("real_assoc_1",num_str @{thm real_assoc_1})
7.14 (*
7.15 Don't use
7.16 - Calc ("HOL.divide", eval_cancel "#divide_e"),
7.17 + Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
7.18 Calc ("Atools.pow" ,eval_binop "#power_"),
7.19 *)
7.20 ];
7.21 @@ -84,11 +84,11 @@
7.22 (*asm_thm = [],*)
7.23 rules = [
7.24 Thm ("real_assoc_1",num_str @{thm real_assoc_1}),
7.25 - Calc ("op +",eval_binop "#add_"),
7.26 - Calc ("op -",eval_binop "#sub_"),
7.27 + Calc ("Groups.plus_class.plus",eval_binop "#add_"),
7.28 + Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
7.29 Calc ("op *",eval_binop "#mult_"),
7.30 (* Dont use
7.31 - Calc ("HOL.divide", eval_cancel "#divide_e"),
7.32 + Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
7.33 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
7.34 *)
7.35 Calc ("Atools.pow" ,eval_binop "#power_")
8.1 --- a/src/Tools/isac/Knowledge/Poly.thy Thu Sep 23 12:56:51 2010 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Thu Sep 23 14:49:23 2010 +0200
8.3 @@ -177,7 +177,7 @@
8.4 let fun coeff_in c v = member op = (vars c) v;
8.5 fun finddivide (_ $ _ $ _ $ _) v = raise error("is_polyrat_in:")
8.6 (* at the moment there is no term like this, but ....*)
8.7 - | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v =
8.8 + | finddivide (t as (Const ("Rings.inverse_class.divide",_) $ _ $ b)) v =
8.9 not(coeff_in b v)
8.10 | finddivide (_ $ t1 $ t2) v =
8.11 (finddivide t1 v) orelse (finddivide t2 v)
8.12 @@ -250,21 +250,21 @@
8.13 (*val it = NONE*)
8.14 ------------------------------------------------------------------*)
8.15 fun expand_deg_in t v =
8.16 - let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) =
8.17 + let fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
8.18 (case mono_deg_in t2 v of (* $ is left associative*)
8.19 SOME d' => edi d' d' t1
8.20 | NONE => NONE)
8.21 - | edi ~1 ~1 (Const ("op -",_) $ t1 $ t2) =
8.22 + | edi ~1 ~1 (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
8.23 (case mono_deg_in t2 v of
8.24 SOME d' => edi d' d' t1
8.25 | NONE => NONE)
8.26 - | edi d dmax (Const ("op -",_) $ t1 $ t2) =
8.27 + | edi d dmax (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
8.28 (case mono_deg_in t2 v of
8.29 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
8.30 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
8.31 then edi d' dmax t1 else NONE
8.32 | NONE => NONE)
8.33 - | edi d dmax (Const ("op +",_) $ t1 $ t2) =
8.34 + | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
8.35 (case mono_deg_in t2 v of
8.36 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
8.37 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
8.38 @@ -297,11 +297,11 @@
8.39 expand_deg_in t v;
8.40 -------------------------------------------------------------------*)
8.41 fun poly_deg_in t v =
8.42 - let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) =
8.43 + let fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
8.44 (case mono_deg_in t2 v of (* $ is left associative*)
8.45 SOME d' => edi d' d' t1
8.46 | NONE => NONE)
8.47 - | edi d dmax (Const ("op +",_) $ t1 $ t2) =
8.48 + | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
8.49 (case mono_deg_in t2 v of
8.50 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
8.51 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
8.52 @@ -399,8 +399,8 @@
8.53 append_rls "Poly_erls" Atools_erls
8.54 [ Calc ("op =",eval_equal "#equal_"),
8.55 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
8.56 - Calc ("op +",eval_binop "#add_"),
8.57 - Calc ("op -",eval_binop "#sub_"),
8.58 + Calc ("Groups.plus_class.plus",eval_binop "#add_"),
8.59 + Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
8.60 Calc ("op *",eval_binop "#mult_"),
8.61 Calc ("Atools.pow" ,eval_binop "#power_")
8.62 ];
8.63 @@ -409,8 +409,8 @@
8.64 append_rls "poly_crls" Atools_crls
8.65 [ Calc ("op =",eval_equal "#equal_"),
8.66 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
8.67 - Calc ("op +",eval_binop "#add_"),
8.68 - Calc ("op -",eval_binop "#sub_"),
8.69 + Calc ("Groups.plus_class.plus",eval_binop "#add_"),
8.70 + Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
8.71 Calc ("op *",eval_binop "#mult_"),
8.72 Calc ("Atools.pow" ,eval_binop "#power_")
8.73 ];
8.74 @@ -553,13 +553,13 @@
8.75 (*.the expression contains + - * ^ only ?
8.76 this is weaker than 'is_polynomial' !.*)
8.77 fun is_polyexp (Free _) = true
8.78 - | is_polyexp (Const ("op +",_) $ Free _ $ Free _) = true
8.79 - | is_polyexp (Const ("op -",_) $ Free _ $ Free _) = true
8.80 + | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
8.81 + | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
8.82 | is_polyexp (Const ("op *",_) $ Free _ $ Free _) = true
8.83 | is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
8.84 - | is_polyexp (Const ("op +",_) $ t1 $ t2) =
8.85 + | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
8.86 ((is_polyexp t1) andalso (is_polyexp t2))
8.87 - | is_polyexp (Const ("op -",_) $ t1 $ t2) =
8.88 + | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
8.89 ((is_polyexp t1) andalso (is_polyexp t2))
8.90 | is_polyexp (Const ("op *",_) $ t1 $ t2) =
8.91 ((is_polyexp t1) andalso (is_polyexp t2))
8.92 @@ -658,12 +658,12 @@
8.93 Rls{id = "calc_add_mult_pow_", preconds = [],
8.94 rew_ord = ("dummy_ord", dummy_ord),
8.95 erls = Atools_erls(*erls3.4.03*),srls = Erls,
8.96 - calc = [("PLUS" , ("op +", eval_binop "#add_")),
8.97 + calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
8.98 ("TIMES" , ("op *", eval_binop "#mult_")),
8.99 ("POWER", ("Atools.pow", eval_binop "#power_"))
8.100 ],
8.101 (*asm_thm = [],*)
8.102 - rules = [Calc ("op +", eval_binop "#add_"),
8.103 + rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"),
8.104 Calc ("op *", eval_binop "#mult_"),
8.105 Calc ("Atools.pow", eval_binop "#power_")
8.106 ], scr = EmptyScr}:rls;
8.107 @@ -689,7 +689,7 @@
8.108 Rls{id = "collect_numerals_", preconds = [],
8.109 rew_ord = ("dummy_ord", dummy_ord),
8.110 erls = Atools_erls, srls = Erls,
8.111 - calc = [("PLUS" , ("op +", eval_binop "#add_"))
8.112 + calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_"))
8.113 ],
8.114 rules =
8.115 [Thm ("real_num_collect",num_str @{thm real_num_collect}),
8.116 @@ -702,7 +702,7 @@
8.117 Thm ("real_one_collect_assoc_r",num_str @{thm real_one_collect_assoc_r}),
8.118 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
8.119
8.120 - Calc ("op +", eval_binop "#add_"),
8.121 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
8.122
8.123 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
8.124 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
8.125 @@ -751,7 +751,7 @@
8.126 Rls{id = "collect_numerals", preconds = [],
8.127 rew_ord = ("dummy_ord", dummy_ord),
8.128 erls = Atools_erls(*erls3.4.03*),srls = Erls,
8.129 - calc = [("PLUS" , ("op +", eval_binop "#add_")),
8.130 + calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
8.131 ("TIMES" , ("op *", eval_binop "#mult_")),
8.132 ("POWER", ("Atools.pow", eval_binop "#power_"))
8.133 ],
8.134 @@ -766,7 +766,7 @@
8.135 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
8.136 (*"m is_const ==> n + (m * n + k) = (1 + m) * n + k"*)
8.137
8.138 - Calc ("op +", eval_binop "#add_"),
8.139 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
8.140
8.141 (*MG am 2.5.03: 2 Theoreme aus reduce_012 hierher verschoben*)
8.142 Thm ("sym_real_mult_2",
8.143 @@ -879,7 +879,7 @@
8.144 Rls{id = "collect_numerals", preconds = [],
8.145 rew_ord = ("dummy_ord", dummy_ord),
8.146 erls = Atools_erls(*erls3.4.03*),srls = Erls,
8.147 - calc = [("PLUS" , ("op +", eval_binop "#add_")),
8.148 + calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
8.149 ("TIMES" , ("op *", eval_binop "#mult_")),
8.150 ("POWER", ("Atools.pow", eval_binop "#power_"))
8.151 ],
8.152 @@ -893,7 +893,7 @@
8.153 (*"m is_const ==> n + m * n = (1 + m) * n"*)
8.154 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
8.155 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
8.156 - Calc ("op +", eval_binop "#add_"),
8.157 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
8.158 Calc ("op *", eval_binop "#mult_"),
8.159 Calc ("Atools.pow", eval_binop "#power_")
8.160 ], scr = EmptyScr}:rls;
8.161 @@ -1024,7 +1024,7 @@
8.162 val expand_binoms =
8.163 Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
8.164 erls = Atools_erls, srls = Erls,
8.165 - calc = [("PLUS" , ("op +", eval_binop "#add_")),
8.166 + calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
8.167 ("TIMES" , ("op *", eval_binop "#mult_")),
8.168 ("POWER", ("Atools.pow", eval_binop "#power_"))
8.169 ],
8.170 @@ -1079,7 +1079,7 @@
8.171 (*"0 * z = 0"*)
8.172 Thm ("add_0_left",num_str @{thm add_0_left}),(*"0 + z = z"*)
8.173
8.174 - Calc ("op +", eval_binop "#add_"),
8.175 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
8.176 Calc ("op *", eval_binop "#mult_"),
8.177 Calc ("Atools.pow", eval_binop "#power_"),
8.178 (*Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
8.179 @@ -1114,7 +1114,7 @@
8.180 num_str @{thm real_one_collect_assoc}),
8.181 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
8.182
8.183 - Calc ("op +", eval_binop "#add_"),
8.184 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
8.185 Calc ("op *", eval_binop "#mult_"),
8.186 Calc ("Atools.pow", eval_binop "#power_")
8.187 ],
8.188 @@ -1127,7 +1127,7 @@
8.189 (*FIXME.0401: make SML-order local to make_polynomial(_) *)
8.190 (*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *)
8.191 (* Polynom --> List von Monomen *)
8.192 -fun poly2list (Const ("op +",_) $ t1 $ t2) =
8.193 +fun poly2list (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
8.194 (poly2list t1) @ (poly2list t2)
8.195 | poly2list t = [t];
8.196
8.197 @@ -1277,7 +1277,7 @@
8.198
8.199 (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt
8.200 (mit gewuenschtem Typen T) *)
8.201 -fun plus T = Const ("op +", [T,T] ---> T);
8.202 +fun plus T = Const ("Groups.plus_class.plus", [T,T] ---> T);
8.203 fun mult T = Const ("op *", [T,T] ---> T);
8.204 fun binop op_ t1 t2 = op_ $ t1 $ t2;
8.205 fun create_prod T (a,b) = binop (mult T) a b;
8.206 @@ -1352,9 +1352,9 @@
8.207 erls = append_rls "e_rls-is_multUnordered" e_rls(*MG: poly_erls*)
8.208 [Calc ("Poly.is'_multUnordered",
8.209 eval_is_multUnordered "")],
8.210 - calc = [("PLUS" , ("op +" , eval_binop "#add_")),
8.211 + calc = [("PLUS" , ("Groups.plus_class.plus" , eval_binop "#add_")),
8.212 ("TIMES" , ("op *" , eval_binop "#mult_")),
8.213 - ("DIVIDE", ("HOL.divide", eval_cancel "#divide_e")),
8.214 + ("DIVIDE", ("Rings.inverse_class.divide", eval_cancel "#divide_e")),
8.215 ("POWER" , ("Atools.pow", eval_binop "#power_"))],
8.216 scr=Rfuns {init_state = init_state,
8.217 normal_form = normal_form,
8.218 @@ -1405,9 +1405,9 @@
8.219 [Calc ("Poly.is'_addUnordered", eval_is_addUnordered "")
8.220 (*WN.18.6.03 definiert in thy,
8.221 evaluiert prepat*)],
8.222 - calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
8.223 + calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
8.224 ("TIMES" ,("op *" ,eval_binop "#mult_")),
8.225 - ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_e")),
8.226 + ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
8.227 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
8.228 (*asm_thm=[],*)
8.229 scr=Rfuns {init_state = init_state,
8.230 @@ -1491,7 +1491,7 @@
8.231 val rev_rew_p =
8.232 Seq{id = "reverse_rewriting", preconds = [], rew_ord = ("termlessI",termlessI),
8.233 erls = Atools_erls, srls = Erls,
8.234 - calc = [(*("PLUS" , ("op +", eval_binop "#add_")),
8.235 + calc = [(*("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
8.236 ("TIMES" , ("op *", eval_binop "#mult_")),
8.237 ("POWER", ("Atools.pow", eval_binop "#power_"))*)
8.238 ],
8.239 @@ -1514,7 +1514,7 @@
8.240 Rls_ order_mult_rls_,
8.241 (*Rls_ order_add_rls_,*)
8.242
8.243 - Calc ("op +", eval_binop "#add_"),
8.244 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
8.245 Calc ("op *", eval_binop "#mult_"),
8.246 Calc ("Atools.pow", eval_binop "#power_"),
8.247
8.248 @@ -1540,7 +1540,7 @@
8.249 Thm ("realpow_multI", num_str @{thm realpow_multI}),
8.250 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
8.251
8.252 - Calc ("op +", eval_binop "#add_"),
8.253 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
8.254 Calc ("op *", eval_binop "#mult_"),
8.255 Calc ("Atools.pow", eval_binop "#power_"),
8.256
9.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Thu Sep 23 12:56:51 2010 +0200
9.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Thu Sep 23 14:49:23 2010 +0200
9.3 @@ -457,10 +457,10 @@
9.4 Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
9.5 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
9.6 Thm ("realpow_multI",num_str @{thm realpow_multI}),
9.7 - Calc ("op +",eval_binop "#add_"),
9.8 - Calc ("op -",eval_binop "#sub_"),
9.9 + Calc ("Groups.plus_class.plus",eval_binop "#add_"),
9.10 + Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
9.11 Calc ("op *",eval_binop "#mult_"),
9.12 - Calc ("HOL.divide", eval_cancel "#divide_e"),
9.13 + Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
9.14 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
9.15 Calc ("Atools.pow" ,eval_binop "#power_"),
9.16 Rls_ reduce_012
9.17 @@ -1481,7 +1481,7 @@
9.18 Rls_ separate_bdvs,
9.19 (* Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*)
9.20 Rls_ cancel_p
9.21 - (*Calc ("HOL.divide" ,eval_cancel "#divide_e") too weak!*)
9.22 + (*Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e") too weak!*)
9.23 ],
9.24 scr = EmptyScr}:rls);
9.25
10.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Thu Sep 23 12:56:51 2010 +0200
10.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Thu Sep 23 14:49:23 2010 +0200
10.3 @@ -262,8 +262,8 @@
10.4 Thm ("subtrahiere_x_minus_minus1",num_str @{thm subtrahiere_x_minus_minus1}),
10.5 (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
10.6
10.7 - Calc ("op +", eval_binop "#add_"),
10.8 - Calc ("op -", eval_binop "#subtr_"),
10.9 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
10.10 + Calc ("Groups.minus_class.minus", eval_binop "#subtr_"),
10.11
10.12 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
10.13 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
10.14 @@ -382,8 +382,8 @@
10.15 val rechnen =
10.16 append_rls "rechnen" e_rls
10.17 [Calc ("op *", eval_binop "#mult_"),
10.18 - Calc ("op +", eval_binop "#add_"),
10.19 - Calc ("op -", eval_binop "#subtr_")
10.20 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
10.21 + Calc ("Groups.minus_class.minus", eval_binop "#subtr_")
10.22 ];
10.23
10.24 ruleset' :=
11.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Thu Sep 23 12:56:51 2010 +0200
11.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Thu Sep 23 14:49:23 2010 +0200
11.3 @@ -52,7 +52,7 @@
11.4 fun coeff_in c v = member op = (vars c) v;
11.5 fun finddivide (_ $ _ $ _ $ _) v = raise error("is_rateqation_in:")
11.6 (* at the moment there is no term like this, but ....*)
11.7 - | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v = coeff_in b v
11.8 + | finddivide (t as (Const ("Rings.inverse_class.divide",_) $ _ $ b)) v = coeff_in b v
11.9 | finddivide (_ $ t1 $ t2) v = (finddivide t1 v)
11.10 orelse (finddivide t2 v)
11.11 | finddivide (_ $ t1) v = (finddivide t1 v)
11.12 @@ -94,7 +94,7 @@
11.13 (merge_rls "is_ratequation_in" calculate_Rational
11.14 (append_rls "is_ratequation_in"
11.15 Poly_erls
11.16 - [(*Calc ("HOL.divide", eval_cancel "#divide_e"),*)
11.17 + [(*Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),*)
11.18 Calc ("RatEq.is'_ratequation'_in",
11.19 eval_is_ratequation_in "")
11.20
11.21 @@ -112,7 +112,7 @@
11.22 (merge_rls "is_ratequation_in" calculate_Rational
11.23 (append_rls "is_ratequation_in"
11.24 Poly_erls
11.25 - [(*Calc ("HOL.divide", eval_cancel "#divide_e"),*)
11.26 + [(*Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),*)
11.27 Calc ("RatEq.is'_ratequation'_in",
11.28 eval_is_ratequation_in "")
11.29 ]))
12.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml Thu Sep 23 12:56:51 2010 +0200
12.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml Thu Sep 23 14:49:23 2010 +0200
12.3 @@ -63,7 +63,7 @@
12.4 else raise error ("term2poly.2 "^term2str t)
12.5 | mono t _ _ = raise error ("term2poly.3 "^term2str t);
12.6
12.7 -fun poly (Const ("op +",_) $ t1 $ t2) v g =
12.8 +fun poly (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v g =
12.9 let val l = mono t1 v g
12.10 in (l @ (poly t2 v ((length l) + g))) end
12.11 | poly t v g = mono t v g;
12.12 @@ -73,7 +73,7 @@
12.13 handle _ => NONE)
12.14 | term2poly (Const ("op *",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v =
12.15 if t = v then SOME [0, (the o int_of_str) s1] else NONE
12.16 - | term2poly (Const ("op +",_) $ (Free (s1,_)) $ t) v =
12.17 + | term2poly (Const ("Groups.plus_class.plus",_) $ (Free (s1,_)) $ t) v =
12.18 SOME ([(the o int_of_str) s1] @ (poly t v 1))
12.19 | term2poly t v =
12.20 SOME (poly t v 0) handle _ => NONE;
12.21 @@ -144,7 +144,7 @@
12.22 (cterm_of thy) t;
12.23
12.24
12.25 -fun mk_sum pT t1 t2 = Const ("op +", [pT, pT]--->pT) $ t1 $ t2;
12.26 +fun mk_sum pT t1 t2 = Const ("Groups.plus_class.plus", [pT, pT]--->pT) $ t1 $ t2;
12.27
12.28
12.29 fun poly2term cT vT pT eT ([p]:poly) v = mk_mono cT vT pT eT p v 0
13.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Sep 23 12:56:51 2010 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Thu Sep 23 14:49:23 2010 +0200
13.3 @@ -1324,7 +1324,7 @@
13.4 | test_polynomial (t as Free(str,_)) v = true
13.5 | test_polynomial (t as Const ("op *",_) $ t1 $ t2) v = if v="^" then false
13.6 else (test_polynomial t1 "*") andalso (test_polynomial t2 "*")
13.7 - | test_polynomial (t as Const ("op +",_) $ t1 $ t2) v = if v="*" orelse v="^" then false
13.8 + | test_polynomial (t as Const ("Groups.plus_class.plus",_) $ t1 $ t2) v = if v="*" orelse v="^" then false
13.9 else (test_polynomial t1 " ") andalso (test_polynomial t2 " ")
13.10 | test_polynomial (t as Const ("Atools.pow",_) $ t1 $ t2) v = (test_polynomial t1 "^") andalso (test_polynomial t2 "^")
13.11 | test_polynomial _ v = false;
13.12 @@ -1337,9 +1337,9 @@
13.13 fun test_exp (t as Free(str,_)) v = true
13.14 | test_exp (t as Const ("op *",_) $ t1 $ t2) v = if v="^" then false
13.15 else (test_exp t1 "*") andalso (test_exp t2 "*")
13.16 - | test_exp (t as Const ("op +",_) $ t1 $ t2) v = if v="*" orelse v="^" then false
13.17 + | test_exp (t as Const ("Groups.plus_class.plus",_) $ t1 $ t2) v = if v="*" orelse v="^" then false
13.18 else (test_exp t1 " ") andalso (test_exp t2 " ")
13.19 - | test_exp (t as Const ("op -",_) $ t1 $ t2) v = if v="*" orelse v="^" then false
13.20 + | test_exp (t as Const ("Groups.minus_class.minus",_) $ t1 $ t2) v = if v="*" orelse v="^" then false
13.21 else (test_exp t1 " ") andalso (test_exp t2 " ")
13.22 | test_exp (t as Const ("Atools.pow",_) $ t1 $ t2) v = (test_exp t1 "^") andalso (test_exp t2 "^")
13.23 | test_exp _ v = false;
13.24 @@ -1429,11 +1429,11 @@
13.25 else raise error ("RATIONALS_TERM2COEF_EXCEPTION 1: Invalid term")
13.26 )
13.27 end
13.28 - | term2coef' (Const ("op +",_) $ t1 $ t2) v :mv_poly option=
13.29 + | term2coef' (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v :mv_poly option=
13.30 (
13.31 SOME ((the(term2coef' t1 v)) @ (the(term2coef' t2 v))) handle _ => NONE
13.32 )
13.33 - | term2coef' (Const ("op -",_) $ t1 $ t2) v :mv_poly option=
13.34 + | term2coef' (Const ("Groups.minus_class.minus",_) $ t1 $ t2) v :mv_poly option=
13.35 (
13.36 SOME ((the(term2coef' t1 v)) @ mv_skalar_mul((the(term2coef' t2 v)),1)) handle _ => NONE
13.37 )
13.38 @@ -1544,11 +1544,11 @@
13.39 else raise error ("RATIONALS_TERM2POLY_EXCEPTION 1: Invalid term")
13.40 )
13.41 end
13.42 - | term2poly' (Const ("op +",_) $ t1 $ t2) v :mv_poly option =
13.43 + | term2poly' (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v :mv_poly option =
13.44 (
13.45 SOME ((the(term2poly' t1 v)) @ (the(term2poly' t2 v))) handle _ => NONE
13.46 )
13.47 - | term2poly' (Const ("op -",_) $ t1 $ t2) v :mv_poly option =
13.48 + | term2poly' (Const ("Groups.minus_class.minus",_) $ t1 $ t2) v :mv_poly option =
13.49 (
13.50 SOME ((the(term2poly' t1 v)) @ mv_skalar_mul((the(term2poly' t2 v)),~1)) handle _ => NONE
13.51 )
13.52 @@ -1674,7 +1674,7 @@
13.53 fun poly2term' ([] : mv_poly, vs) = Free(str_of_int 0, HOLogic.realT)
13.54 | poly2term' ([(c, e) : mv_monom], vs) = monom2term ((c, e), vs)
13.55 | poly2term' ((c, e) :: ces, vs) =
13.56 - Const("op +", [HOLogic.realT, HOLogic.realT] ---> HOLogic.realT) $
13.57 + Const("Groups.plus_class.plus", [HOLogic.realT, HOLogic.realT] ---> HOLogic.realT) $
13.58 poly2term (ces, vs) $ monom2term ((c, e), vs)
13.59 and poly2term (xs, vs) = poly2term' (rev (sort (mv_geq LEX_) (xs)), vs);
13.60
13.61 @@ -1709,13 +1709,13 @@
13.62 | exp2term' ([(c,e)],vars) = monom2term((c,e),vars)
13.63 | exp2term' ((c1,e1)::others,vars) =
13.64 if c1<0 then
13.65 - Const("op -",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.66 + Const("Groups.minus_class.minus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.67 exp2term'(others,vars) $
13.68 (
13.69 monom2term2((c1,e1),vars)
13.70 )
13.71 else
13.72 - Const("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.73 + Const("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.74 exp2term'(others,vars) $
13.75 (
13.76 monom2term2((c1,e1),vars)
13.77 @@ -1743,7 +1743,7 @@
13.78
13.79
13.80 (*. calculates the greatest common divisor of numerator and denominator and seperates it from each .*)
13.81 -fun step_cancel (t as Const ("HOL.divide",_) $ p1 $ p2) =
13.82 +fun step_cancel (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) =
13.83 let
13.84 val p1' = Unsynchronized.ref [];
13.85 val p2' = Unsynchronized.ref [];
13.86 @@ -1756,7 +1756,7 @@
13.87 p3:= sort (mv_geq LEX_) (mv_gcd (!p1') (!p2'));
13.88 if (!p3)=[(1,mv_null2(vars))] then
13.89 (
13.90 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2
13.91 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2
13.92 )
13.93 else
13.94 (
13.95 @@ -1766,7 +1766,7 @@
13.96
13.97 if #1(hd(sort (mv_geq LEX_) (!p2'))) (*mv_lc2(!p2',LEX_)*)>0 then
13.98 (
13.99 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.100 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.101 $
13.102 (
13.103 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.104 @@ -1786,7 +1786,7 @@
13.105 p2':=mv_skalar_mul(!p2',~1);
13.106 p3:=mv_skalar_mul(!p3,~1);
13.107 (
13.108 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.109 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.110 $
13.111 (
13.112 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.113 @@ -1808,7 +1808,7 @@
13.114
13.115
13.116 (*. same as step_cancel, this time for expanded forms (input+output) .*)
13.117 -fun step_cancel_expanded (t as Const ("HOL.divide",_) $ p1 $ p2) =
13.118 +fun step_cancel_expanded (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) =
13.119 let
13.120 val p1' = Unsynchronized.ref [];
13.121 val p2' = Unsynchronized.ref [];
13.122 @@ -1821,7 +1821,7 @@
13.123 p3:= sort (mv_geq LEX_) (mv_gcd (!p1') (!p2'));
13.124 if (!p3)=[(1,mv_null2(vars))] then
13.125 (
13.126 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2
13.127 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2
13.128 )
13.129 else
13.130 (
13.131 @@ -1831,7 +1831,7 @@
13.132
13.133 if #1(hd(sort (mv_geq LEX_) (!p2')))(* mv_lc2(!p2',LEX_)*)>0 then
13.134 (
13.135 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.136 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.137 $
13.138 (
13.139 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.140 @@ -1851,7 +1851,7 @@
13.141 p2':=mv_skalar_mul(!p2',~1);
13.142 p3:=mv_skalar_mul(!p3,~1);
13.143 (
13.144 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.145 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.146 $
13.147 (
13.148 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.149 @@ -1872,7 +1872,7 @@
13.150 | step_cancel_expanded _ = raise error ("RATIONALS_STEP_CANCEL_EXCEPTION: Invalid fraction");
13.151
13.152 (*. calculates the greatest common divisor of numerator and denominator and divides each through it .*)
13.153 -fun direct_cancel (t as Const ("HOL.divide",_) $ p1 $ p2) =
13.154 +fun direct_cancel (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) =
13.155 let
13.156 val p1' = Unsynchronized.ref [];
13.157 val p2' = Unsynchronized.ref [];
13.158 @@ -1886,7 +1886,7 @@
13.159
13.160 if (!p3)=[(1,mv_null2(vars))] then
13.161 (
13.162 - (Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2,[])
13.163 + (Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2,[])
13.164 )
13.165 else
13.166 (
13.167 @@ -1895,7 +1895,7 @@
13.168 if #1(hd(sort (mv_geq LEX_) (!p2'))) (*mv_lc2(!p2',LEX_)*)>0 then
13.169 (
13.170 (
13.171 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.172 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.173 $
13.174 (
13.175 poly2term((!p1'),vars)
13.176 @@ -1926,7 +1926,7 @@
13.177 p2':=mv_skalar_mul(!p2',~1);
13.178 if length(!p3)> 2*(count_neg(!p3)) then () else p3 :=mv_skalar_mul(!p3,~1);
13.179 (
13.180 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.181 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.182 $
13.183 (
13.184 poly2term((!p1'),vars)
13.185 @@ -1957,7 +1957,7 @@
13.186 | direct_cancel _ = raise error ("RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction");
13.187
13.188 (*. same es direct_cancel, this time for expanded forms (input+output).*)
13.189 -fun direct_cancel_expanded (t as Const ("HOL.divide",_) $ p1 $ p2) =
13.190 +fun direct_cancel_expanded (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) =
13.191 let
13.192 val p1' = Unsynchronized.ref [];
13.193 val p2' = Unsynchronized.ref [];
13.194 @@ -1971,7 +1971,7 @@
13.195
13.196 if (!p3)=[(1,mv_null2(vars))] then
13.197 (
13.198 - (Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2,[])
13.199 + (Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2,[])
13.200 )
13.201 else
13.202 (
13.203 @@ -1980,7 +1980,7 @@
13.204 if #1(hd(sort (mv_geq LEX_) (!p2'))) (*mv_lc2(!p2',LEX_)*)>0 then
13.205 (
13.206 (
13.207 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.208 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.209 $
13.210 (
13.211 poly2expanded((!p1'),vars)
13.212 @@ -2011,7 +2011,7 @@
13.213 p2':=mv_skalar_mul(!p2',~1);
13.214 if length(!p3)> 2*(count_neg(!p3)) then () else p3 :=mv_skalar_mul(!p3,~1);
13.215 (
13.216 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.217 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.218 $
13.219 (
13.220 poly2expanded((!p1'),vars)
13.221 @@ -2043,7 +2043,7 @@
13.222
13.223
13.224 (*. adds two fractions .*)
13.225 -fun add_fract ((Const("HOL.divide",_) $ t11 $ t12),(Const("HOL.divide",_) $ t21 $ t22)) =
13.226 +fun add_fract ((Const("Rings.inverse_class.divide",_) $ t11 $ t12),(Const("Rings.inverse_class.divide",_) $ t21 $ t22)) =
13.227 let
13.228 val vars=get_vars(t11) union get_vars(t12) union get_vars(t21) union get_vars(t22);
13.229 val t11'= Unsynchronized.ref (the(term2poly t11 vars));
13.230 @@ -2074,7 +2074,7 @@
13.231 LEX_));
13.232 writeln"### add_fract: done sort mv_add";
13.233 (
13.234 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.235 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.236 $
13.237 (
13.238 poly2term((!nom),vars)
13.239 @@ -2089,7 +2089,7 @@
13.240 | add_fract (_,_) = raise error ("RATIONALS_ADD_FRACTION_EXCEPTION: Invalid add_fraction call");
13.241
13.242 (*. adds two expanded fractions .*)
13.243 -fun add_fract_exp ((Const("HOL.divide",_) $ t11 $ t12),(Const("HOL.divide",_) $ t21 $ t22)) =
13.244 +fun add_fract_exp ((Const("Rings.inverse_class.divide",_) $ t11 $ t12),(Const("Rings.inverse_class.divide",_) $ t21 $ t22)) =
13.245 let
13.246 val vars=get_vars(t11) union get_vars(t12) union get_vars(t21) union get_vars(t22);
13.247 val t11'= Unsynchronized.ref (the(expanded2poly t11 vars));
13.248 @@ -2108,7 +2108,7 @@
13.249 m2 :=sort (mv_geq LEX_) (#1(mv_division(!den,!t22',LEX_)));
13.250 nom :=sort (mv_geq LEX_) (mv_shorten(mv_add(mv_mul(!t11',!m1,LEX_),mv_mul(!t21',!m2,LEX_),LEX_),LEX_));
13.251 (
13.252 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.253 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.254 $
13.255 (
13.256 poly2expanded((!nom),vars)
13.257 @@ -2166,11 +2166,11 @@
13.258
13.259 (*. converts a list of terms to a list of mv_poly .*)
13.260 fun t2d([],_)=[]
13.261 - | t2d((t as (Const("HOL.divide",_) $ p1 $ p2))::xs,vars)= (the(term2poly p2 vars)) :: t2d(xs,vars);
13.262 + | t2d((t as (Const("Rings.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(term2poly p2 vars)) :: t2d(xs,vars);
13.263
13.264 (*. same as t2d, this time for expanded forms .*)
13.265 fun t2d_exp([],_)=[]
13.266 - | t2d_exp((t as (Const("HOL.divide",_) $ p1 $ p2))::xs,vars)= (the(expanded2poly p2 vars)) :: t2d_exp(xs,vars);
13.267 + | t2d_exp((t as (Const("Rings.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(expanded2poly p2 vars)) :: t2d_exp(xs,vars);
13.268
13.269 (*. converts a list of fract terms to a list of their denominators .*)
13.270 fun termlist2denominators [] = ([],[])
13.271 @@ -2183,7 +2183,7 @@
13.272 while length(!xxs)>0 do
13.273 (
13.274 let
13.275 - val (t as Const ("HOL.divide",_) $ p1x $ p2x)=hd(!xxs);
13.276 + val (t as Const ("Rings.inverse_class.divide",_) $ p1x $ p2x)=hd(!xxs);
13.277 in
13.278 (
13.279 xxs:=tl(!xxs);
13.280 @@ -2200,11 +2200,11 @@
13.281
13.282 (*. converts a list of terms to a list of mv_poly .*)
13.283 fun t2d([],_)=[]
13.284 - | t2d((t as (Const("HOL.divide",_) $ p1 $ p2))::xs,vars)= (the(term2poly p2 vars)) :: t2d(xs,vars);
13.285 + | t2d((t as (Const("Rings.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(term2poly p2 vars)) :: t2d(xs,vars);
13.286
13.287 (*. same as t2d, this time for expanded forms .*)
13.288 fun t2d_exp([],_)=[]
13.289 - | t2d_exp((t as (Const("HOL.divide",_) $ p1 $ p2))::xs,vars)= (the(expanded2poly p2 vars)) :: t2d_exp(xs,vars);
13.290 + | t2d_exp((t as (Const("Rings.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(expanded2poly p2 vars)) :: t2d_exp(xs,vars);
13.291
13.292 (*. converts a list of fract terms to a list of their denominators .*)
13.293 fun termlist2denominators [] = ([],[])
13.294 @@ -2217,7 +2217,7 @@
13.295 while length(!xxs)>0 do
13.296 (
13.297 let
13.298 - val (t as Const ("HOL.divide",_) $ p1x $ p2x)=hd(!xxs);
13.299 + val (t as Const ("Rings.inverse_class.divide",_) $ p1x $ p2x)=hd(!xxs);
13.300 in
13.301 (
13.302 xxs:=tl(!xxs);
13.303 @@ -2239,7 +2239,7 @@
13.304 while length(!xxs)>0 do
13.305 (
13.306 let
13.307 - val (t as Const ("HOL.divide",_) $ p1x $ p2x)=hd(!xxs);
13.308 + val (t as Const ("Rings.inverse_class.divide",_) $ p1x $ p2x)=hd(!xxs);
13.309 in
13.310 (
13.311 xxs:=tl(!xxs);
13.312 @@ -2253,7 +2253,7 @@
13.313 (*. reduces all fractions to the least common denominator .*)
13.314 fun com_den(x::xs,denom,den,var)=
13.315 let
13.316 - val (t as Const ("HOL.divide",_) $ p1' $ p2')=x;
13.317 + val (t as Const ("Rings.inverse_class.divide",_) $ p1' $ p2')=x;
13.318 val p2= sort (mv_geq LEX_) (the(term2poly p2' var));
13.319 val p3= #1(mv_division(denom,p2,LEX_));
13.320 val p1var=get_vars(p1');
13.321 @@ -2261,10 +2261,10 @@
13.322 if length(xs)>0 then
13.323 if p3=[(1,mv_null2(var))] then
13.324 (
13.325 - Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.326 + Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.327 $
13.328 (
13.329 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.330 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.331 $
13.332 poly2term(the (term2poly p1' p1var),p1var)
13.333 $
13.334 @@ -2277,10 +2277,10 @@
13.335 )
13.336 else
13.337 (
13.338 - Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.339 + Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.340 $
13.341 (
13.342 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.343 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.344 $
13.345 (
13.346 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.347 @@ -2301,7 +2301,7 @@
13.348 if p3=[(1,mv_null2(var))] then
13.349 (
13.350 (
13.351 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.352 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.353 $
13.354 poly2term(the (term2poly p1' p1var),p1var)
13.355 $
13.356 @@ -2312,7 +2312,7 @@
13.357 )
13.358 else
13.359 (
13.360 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.361 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.362 $
13.363 (
13.364 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.365 @@ -2329,7 +2329,7 @@
13.366 (*. same as com_den, this time for expanded forms .*)
13.367 fun com_den_exp(x::xs,denom,den,var)=
13.368 let
13.369 - val (t as Const ("HOL.divide",_) $ p1' $ p2')=x;
13.370 + val (t as Const ("Rings.inverse_class.divide",_) $ p1' $ p2')=x;
13.371 val p2= sort (mv_geq LEX_) (the(expanded2poly p2' var));
13.372 val p3= #1(mv_division(denom,p2,LEX_));
13.373 val p1var=get_vars(p1');
13.374 @@ -2337,10 +2337,10 @@
13.375 if length(xs)>0 then
13.376 if p3=[(1,mv_null2(var))] then
13.377 (
13.378 - Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.379 + Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.380 $
13.381 (
13.382 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.383 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.384 $
13.385 poly2expanded(the(expanded2poly p1' p1var),p1var)
13.386 $
13.387 @@ -2353,10 +2353,10 @@
13.388 )
13.389 else
13.390 (
13.391 - Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.392 + Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.393 $
13.394 (
13.395 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.396 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.397 $
13.398 (
13.399 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.400 @@ -2377,7 +2377,7 @@
13.401 if p3=[(1,mv_null2(var))] then
13.402 (
13.403 (
13.404 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.405 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.406 $
13.407 poly2expanded(the(expanded2poly p1' p1var),p1var)
13.408 $
13.409 @@ -2388,7 +2388,7 @@
13.410 )
13.411 else
13.412 (
13.413 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.414 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
13.415 $
13.416 (
13.417 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.418 @@ -2407,7 +2407,7 @@
13.419 (* WN0210???SK brauch ma des überhaupt *)
13.420 fun com_den2(x::xs,denom,den,var)=
13.421 let
13.422 - val (t as Const ("HOL.divide",_) $ p1' $ p2')=x;
13.423 + val (t as Const ("Rings.inverse_class.divide",_) $ p1' $ p2')=x;
13.424 val p2= sort (mv_geq LEX_) (the(term2poly p2' var));
13.425 val p3= #1(mv_division(denom,p2,LEX_));
13.426 val p1var=get_vars(p1');
13.427 @@ -2415,13 +2415,13 @@
13.428 if length(xs)>0 then
13.429 if p3=[(1,mv_null2(var))] then
13.430 (
13.431 - Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.432 + Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.433 poly2term(the(term2poly p1' p1var),p1var) $
13.434 com_den2(xs,denom,den,var)
13.435 )
13.436 else
13.437 (
13.438 - Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.439 + Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.440 (
13.441 let
13.442 val p3'=poly2term(p3,var);
13.443 @@ -2451,7 +2451,7 @@
13.444 (* WN0210???SK brauch ma des überhaupt *)
13.445 fun com_den_exp2(x::xs,denom,den,var)=
13.446 let
13.447 - val (t as Const ("HOL.divide",_) $ p1' $ p2')=x;
13.448 + val (t as Const ("Rings.inverse_class.divide",_) $ p1' $ p2')=x;
13.449 val p2= sort (mv_geq LEX_) (the(expanded2poly p2' var));
13.450 val p3= #1(mv_division(denom,p2,LEX_));
13.451 val p1var=get_vars p1';
13.452 @@ -2459,13 +2459,13 @@
13.453 if length(xs)>0 then
13.454 if p3=[(1,mv_null2(var))] then
13.455 (
13.456 - Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.457 + Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.458 poly2expanded(the (expanded2poly p1' p1var),p1var) $
13.459 com_den_exp2(xs,denom,den,var)
13.460 )
13.461 else
13.462 (
13.463 - Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.464 + Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.465 (
13.466 let
13.467 val p3'=poly2expanded(p3,var);
13.468 @@ -2644,7 +2644,7 @@
13.469 val den=factorize_den(#1(den_list),denom,var); (* faktorisierter Nenner !!! *)
13.470 in
13.471 (
13.472 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.473 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.474 com_den2(xs,denom, poly2term(denom,var)(*den*),var) $
13.475 poly2term(denom,var)
13.476 ,
13.477 @@ -2662,7 +2662,7 @@
13.478 val den=factorize_den_exp(#1(den_list),denom,var); (* faktorisierter Nenner !!! *)
13.479 in
13.480 (
13.481 - Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.482 + Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.483 com_den_exp2(xs,denom, poly2term(denom,var)(*den*),var) $
13.484 poly2expanded(denom,var)
13.485 ,
13.486 @@ -2673,21 +2673,21 @@
13.487
13.488
13.489 (*. converts a term, which contains severel terms seperated by +, into a list of these terms .*)
13.490 -fun term2list (t as (Const("HOL.divide",_) $ _ $ _)) = [t]
13.491 +fun term2list (t as (Const("Rings.inverse_class.divide",_) $ _ $ _)) = [t]
13.492 | term2list (t as (Const("Atools.pow",_) $ _ $ _)) =
13.493 - [Const("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.494 + [Const("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.495 t $ Free("1",HOLogic.realT)
13.496 ]
13.497 | term2list (t as (Free(_,_))) =
13.498 - [Const("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.499 + [Const("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.500 t $ Free("1",HOLogic.realT)
13.501 ]
13.502 | term2list (t as (Const("op *",_) $ _ $ _)) =
13.503 - [Const("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.504 + [Const("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
13.505 t $ Free("1",HOLogic.realT)
13.506 ]
13.507 - | term2list (Const("op +",_) $ t1 $ t2) = term2list(t1) @ term2list(t2)
13.508 - | term2list (Const("op -",_) $ t1 $ t2) =
13.509 + | term2list (Const("Groups.plus_class.plus",_) $ t1 $ t2) = term2list(t1) @ term2list(t2)
13.510 + | term2list (Const("Groups.minus_class.minus",_) $ t1 $ t2) =
13.511 raise error ("RATIONALS_TERM2LIST_EXCEPTION: - not implemented yet")
13.512 | term2list _ = raise error ("RATIONALS_TERM2LIST_EXCEPTION: invalid term");
13.513
13.514 @@ -2780,7 +2780,7 @@
13.515 erls = calc_rat_erls, srls = Erls, (*asm_thm = [],*)
13.516 calc = [],
13.517 rules =
13.518 - [Calc ("HOL.divide" ,eval_cancel "#divide_e"),
13.519 + [Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"),
13.520
13.521 Thm ("minus_divide_left",
13.522 num_str (@{thm minus_divide_left} RS @{thm sym})),
13.523 @@ -3001,9 +3001,9 @@
13.524 rew_ord=("ord_make_polynomial",
13.525 ord_make_polynomial false thy),
13.526 erls = rational_erls,
13.527 - calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
13.528 + calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
13.529 ("TIMES" ,("op *" ,eval_binop "#mult_")),
13.530 - ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_e")),
13.531 + ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
13.532 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
13.533 (*asm_thm=[("real_mult_div_cancel2","")],*)
13.534 scr=Rfuns {init_state = init_state thy Atools_erls ro,
13.535 @@ -3083,9 +3083,9 @@
13.536 rew_ord=("ord_make_polynomial",
13.537 ord_make_polynomial false thy),
13.538 erls = rational_erls,
13.539 - calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
13.540 + calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
13.541 ("TIMES" ,("op *" ,eval_binop "#mult_")),
13.542 - ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_e")),
13.543 + ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
13.544 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
13.545 scr=Rfuns {init_state = init_state thy Atools_erls ro,
13.546 normal_form = cancel_ thy,
13.547 @@ -3235,9 +3235,9 @@
13.548 rew_ord=("ord_make_polynomial",
13.549 ord_make_polynomial false thy),
13.550 erls = rational_erls,
13.551 - calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
13.552 + calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
13.553 ("TIMES" ,("op *" ,eval_binop "#mult_")),
13.554 - ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_e")),
13.555 + ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
13.556 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
13.557 scr=Rfuns {init_state = init_state thy Atools_erls ro,
13.558 normal_form = add_fraction_p_ thy,(*FIXME.WN0211*)
13.559 @@ -3383,9 +3383,9 @@
13.560 rew_ord=("ord_make_polynomial",
13.561 ord_make_polynomial false thy),
13.562 erls = rational_erls,
13.563 - calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
13.564 + calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
13.565 ("TIMES" ,("op *" ,eval_binop "#mult_")),
13.566 - ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_e")),
13.567 + ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
13.568 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
13.569 (*asm_thm=[("real_mult_div_cancel2","")],*)
13.570 scr=Rfuns {init_state = init_state thy Atools_erls ro,
13.571 @@ -3402,20 +3402,20 @@
13.572
13.573 (*.the expression contains + - * ^ / only ?.*)
13.574 fun is_ratpolyexp (Free _) = true
13.575 - | is_ratpolyexp (Const ("op +",_) $ Free _ $ Free _) = true
13.576 - | is_ratpolyexp (Const ("op -",_) $ Free _ $ Free _) = true
13.577 + | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
13.578 + | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
13.579 | is_ratpolyexp (Const ("op *",_) $ Free _ $ Free _) = true
13.580 | is_ratpolyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
13.581 - | is_ratpolyexp (Const ("HOL.divide",_) $ Free _ $ Free _) = true
13.582 - | is_ratpolyexp (Const ("op +",_) $ t1 $ t2) =
13.583 + | is_ratpolyexp (Const ("Rings.inverse_class.divide",_) $ Free _ $ Free _) = true
13.584 + | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
13.585 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
13.586 - | is_ratpolyexp (Const ("op -",_) $ t1 $ t2) =
13.587 + | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
13.588 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
13.589 | is_ratpolyexp (Const ("op *",_) $ t1 $ t2) =
13.590 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
13.591 | is_ratpolyexp (Const ("Atools.pow",_) $ t1 $ t2) =
13.592 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
13.593 - | is_ratpolyexp (Const ("HOL.divide",_) $ t1 $ t2) =
13.594 + | is_ratpolyexp (Const ("Rings.inverse_class.divide",_) $ t1 $ t2) =
13.595 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
13.596 | is_ratpolyexp _ = false;
13.597
13.598 @@ -3462,7 +3462,7 @@
13.599 Calc ("op <",eval_equ "#less_"),
13.600 Thm ("not_false", num_str @{thm not_false}),
13.601 Thm ("not_true", num_str @{thm not_true}),
13.602 - Calc ("op +",eval_binop "#add_")
13.603 + Calc ("Groups.plus_class.plus",eval_binop "#add_")
13.604 ],
13.605 scr = EmptyScr
13.606 }:rls);
13.607 @@ -3495,7 +3495,7 @@
13.608 (*"[| 1 < n; not(r is_atom) |]==>r ^^^ n = r * r ^^^ (n + -1)"*)
13.609 Thm ("realpow_eq_oneI",num_str @{thm realpow_eq_oneI}),
13.610 (*"1 ^^^ n = 1"*)
13.611 - Calc ("op +",eval_binop "#add_")
13.612 + Calc ("Groups.plus_class.plus",eval_binop "#add_")
13.613 ],
13.614 scr = EmptyScr
13.615 }:rls);
13.616 @@ -3519,7 +3519,7 @@
13.617 Thm ("divide_divide_eq_left",
13.618 num_str @{thm divide_divide_eq_left}),
13.619 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
13.620 - Calc ("HOL.divide" ,eval_cancel "#divide_e")
13.621 + Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e")
13.622 ],
13.623 scr = EmptyScr
13.624 }:rls);
13.625 @@ -3695,7 +3695,7 @@
13.626 Thm ("divide_divide_eq_left",
13.627 num_str @{thm divide_divide_eq_left}),
13.628 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
13.629 - Calc ("HOL.divide" ,eval_cancel "#divide_e"),
13.630 + Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"),
13.631
13.632 Thm ("rat_power", num_str @{thm rat_power})
13.633 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
14.1 --- a/src/Tools/isac/Knowledge/Root.thy Thu Sep 23 12:56:51 2010 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Root.thy Thu Sep 23 14:49:23 2010 +0200
14.3 @@ -168,10 +168,10 @@
14.4 append_rls "Root_crls" Atools_erls
14.5 [Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
14.6 Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"),
14.7 - Calc ("HOL.divide",eval_cancel "#divide_e"),
14.8 + Calc ("Rings.inverse_class.divide",eval_cancel "#divide_e"),
14.9 Calc ("Atools.pow" ,eval_binop "#power_"),
14.10 - Calc ("op +", eval_binop "#add_"),
14.11 - Calc ("op -", eval_binop "#sub_"),
14.12 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
14.13 + Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
14.14 Calc ("op *", eval_binop "#mult_"),
14.15 Calc ("op =",eval_equal "#equal_")
14.16 ];
14.17 @@ -180,10 +180,10 @@
14.18 append_rls "Root_erls" Atools_erls
14.19 [Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
14.20 Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"),
14.21 - Calc ("HOL.divide",eval_cancel "#divide_e"),
14.22 + Calc ("Rings.inverse_class.divide",eval_cancel "#divide_e"),
14.23 Calc ("Atools.pow" ,eval_binop "#power_"),
14.24 - Calc ("op +", eval_binop "#add_"),
14.25 - Calc ("op -", eval_binop "#sub_"),
14.26 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
14.27 + Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
14.28 Calc ("op *", eval_binop "#mult_"),
14.29 Calc ("op =",eval_equal "#equal_")
14.30 ];
14.31 @@ -251,7 +251,7 @@
14.32 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
14.33 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
14.34
14.35 - Calc ("op +", eval_binop "#add_"),
14.36 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
14.37 Calc ("op *", eval_binop "#mult_"),
14.38 Calc ("Atools.pow", eval_binop "#power_")
14.39 ],
14.40 @@ -296,10 +296,10 @@
14.41 Thm ("add_0_left",num_str @{thm add_0_left}),
14.42 (*"0 + z = z"*)
14.43
14.44 - Calc ("op +", eval_binop "#add_"),
14.45 - Calc ("op -", eval_binop "#sub_"),
14.46 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
14.47 + Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
14.48 Calc ("op *", eval_binop "#mult_"),
14.49 - Calc ("HOL.divide" ,eval_cancel "#divide_e"),
14.50 + Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"),
14.51 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
14.52 Calc ("Atools.pow", eval_binop "#power_"),
14.53
14.54 @@ -321,10 +321,10 @@
14.55 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
14.56 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
14.57
14.58 - Calc ("op +", eval_binop "#add_"),
14.59 - Calc ("op -", eval_binop "#sub_"),
14.60 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
14.61 + Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
14.62 Calc ("op *", eval_binop "#mult_"),
14.63 - Calc ("HOL.divide" ,eval_cancel "#divide_e"),
14.64 + Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"),
14.65 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
14.66 Calc ("Atools.pow", eval_binop "#power_")
14.67 ],
15.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Thu Sep 23 12:56:51 2010 +0200
15.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Thu Sep 23 14:49:23 2010 +0200
15.3 @@ -156,10 +156,10 @@
15.4 fun coeff_in c v = member op = (vars c) v;
15.5 fun isnorm (_ $ _ $ _ $ _) v = raise error("is_normSqrtTerm_in:")
15.6 (* at the moment there is no term like this, but ....*)
15.7 - | isnorm (Const ("op +",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
15.8 + | isnorm (Const ("Groups.plus_class.plus",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
15.9 | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
15.10 - | isnorm (Const ("op -",_) $ _ $ _) v = false
15.11 - | isnorm (Const ("HOL.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse
15.12 + | isnorm (Const ("Groups.minus_class.minus",_) $ _ $ _) v = false
15.13 + | isnorm (Const ("Rings.inverse_class.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse
15.14 (is_sqrtTerm_in t2 v)
15.15 | isnorm (Const ("NthRoot.sqrt",_) $ t1) v = coeff_in t1 v
15.16 | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v
15.17 @@ -445,10 +445,10 @@
15.18 (* a+(b+c) = a+b+c *)
15.19 Thm ("real_assoc_2",num_str @{thm real_assoc_2}),
15.20 (* a*(b*c) = a*b*c *)
15.21 - Calc ("op +",eval_binop "#add_"),
15.22 - Calc ("op -",eval_binop "#sub_"),
15.23 + Calc ("Groups.plus_class.plus",eval_binop "#add_"),
15.24 + Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
15.25 Calc ("op *",eval_binop "#mult_"),
15.26 - Calc ("HOL.divide", eval_cancel "#divide_e"),
15.27 + Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
15.28 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
15.29 Calc ("Atools.pow" ,eval_binop "#power_"),
15.30 Thm("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),
16.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Thu Sep 23 12:56:51 2010 +0200
16.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Thu Sep 23 14:49:23 2010 +0200
16.3 @@ -43,14 +43,14 @@
16.4 fun is_rootRatAddTerm_in t v =
16.5 let
16.6 fun coeff_in c v = member op = (vars c) v;
16.7 - fun rootadd (t as (Const ("op +",_) $ t2 $ t3)) v =
16.8 + fun rootadd (t as (Const ("Groups.plus_class.plus",_) $ t2 $ t3)) v =
16.9 (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)
16.10 - | rootadd (t as (Const ("op -",_) $ t2 $ t3)) v =
16.11 + | rootadd (t as (Const ("Groups.minus_class.minus",_) $ t2 $ t3)) v =
16.12 (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)
16.13 | rootadd _ _ = false;
16.14 fun findrootrat (_ $ _ $ _ $ _) v = raise error("is_rootRatAddTerm_in:")
16.15 (* at the moment there is no term like this, but ....*)
16.16 - | findrootrat (t as (Const ("HOL.divide",_) $ _ $ t3)) v =
16.17 + | findrootrat (t as (Const ("Rings.inverse_class.divide",_) $ _ $ t3)) v =
16.18 if (is_rootTerm_in t3 v) then rootadd t3 v else false
16.19 | findrootrat (_ $ t1 $ t2) v =
16.20 (findrootrat t1 v) orelse (findrootrat t2 v)
17.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Sep 23 12:56:51 2010 +0200
17.2 +++ b/src/Tools/isac/Knowledge/Test.thy Thu Sep 23 14:49:23 2010 +0200
17.3 @@ -227,7 +227,7 @@
17.4 Calc ("Atools.is'_const",eval_const "#is_const_"),
17.5 Calc ("Tools.matches",eval_matches ""),
17.6
17.7 - Calc ("op +",eval_binop "#add_"),
17.8 + Calc ("Groups.plus_class.plus",eval_binop "#add_"),
17.9 Calc ("op *",eval_binop "#mult_"),
17.10 Calc ("Atools.pow" ,eval_binop "#power_"),
17.11
17.12 @@ -272,7 +272,7 @@
17.13 Calc ("Test.contains'_root",
17.14 eval_contains_root"#contains_root_"),
17.15
17.16 - Calc ("op +",eval_binop "#add_"),
17.17 + Calc ("Groups.plus_class.plus",eval_binop "#add_"),
17.18 Calc ("op *",eval_binop "#mult_"),
17.19 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
17.20 Calc ("Atools.pow" ,eval_binop "#power_"),
17.21 @@ -406,9 +406,9 @@
17.22 Thm ("radd_real_const",num_str @{thm radd_real_const}),
17.23 (* these 2 rules are invers to distr_div_right wrt. termination.
17.24 thus they MUST be done IMMEDIATELY before calc *)
17.25 - Calc ("op +", eval_binop "#add_"),
17.26 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
17.27 Calc ("op *", eval_binop "#mult_"),
17.28 - Calc ("HOL.divide", eval_cancel "#divide_e"),
17.29 + Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
17.30 Calc ("Atools.pow", eval_binop "#power_"),
17.31
17.32 Thm ("rcollect_right",num_str @{thm rcollect_right}),
17.33 @@ -476,7 +476,7 @@
17.34 ML {*
17.35
17.36 (* association list for calculate_, calculate
17.37 - "op +" etc. not usable in scripts *)
17.38 + "Groups.plus_class.plus" etc. not usable in scripts *)
17.39 val calclist =
17.40 [
17.41 (*as Tools.ML*)
17.42 @@ -484,9 +484,9 @@
17.43 ("matches",("Tools.matches",eval_matches "#matches_")),
17.44 ("lhs" ,("Tools.lhs" ,eval_lhs "")),
17.45 (*aus Atools.ML*)
17.46 - ("PLUS" ,("op +" ,eval_binop "#add_")),
17.47 + ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
17.48 ("TIMES" ,("op *" ,eval_binop "#mult_")),
17.49 - ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_e")),
17.50 + ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
17.51 ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
17.52 ("is_const",("Atools.is'_const",eval_const "#is_const_")),
17.53 ("le" ,("op <" ,eval_equ "#less_")),
17.54 @@ -1295,7 +1295,7 @@
17.55 Rls{id = "make_polytest", preconds = []:term list,
17.56 rew_ord = ("ord_make_polytest", ord_make_polytest false (theory "Poly")),
17.57 erls = testerls, srls = Erls,
17.58 - calc = [("PLUS" , ("op +", eval_binop "#add_")),
17.59 + calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
17.60 ("TIMES" , ("op *", eval_binop "#mult_")),
17.61 ("POWER", ("Atools.pow", eval_binop "#power_"))
17.62 ],
17.63 @@ -1352,7 +1352,7 @@
17.64 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
17.65 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
17.66
17.67 - Calc ("op +", eval_binop "#add_"),
17.68 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
17.69 Calc ("op *", eval_binop "#mult_"),
17.70 Calc ("Atools.pow", eval_binop "#power_")
17.71 ],
17.72 @@ -1401,7 +1401,7 @@
17.73 Rls{id = "expand_binomtest", preconds = [],
17.74 rew_ord = ("termlessI",termlessI),
17.75 erls = testerls, srls = Erls,
17.76 - calc = [("PLUS" , ("op +", eval_binop "#add_")),
17.77 + calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
17.78 ("TIMES" , ("op *", eval_binop "#mult_")),
17.79 ("POWER", ("Atools.pow", eval_binop "#power_"))
17.80 ],
17.81 @@ -1452,7 +1452,7 @@
17.82 Thm ("add_0_left",num_str @{thm add_0_left}),
17.83 (*"0 + z = z"*)
17.84
17.85 - Calc ("op +", eval_binop "#add_"),
17.86 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
17.87 Calc ("op *", eval_binop "#mult_"),
17.88 Calc ("Atools.pow", eval_binop "#power_"),
17.89 (*
17.90 @@ -1485,7 +1485,7 @@
17.91 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
17.92 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
17.93
17.94 - Calc ("op +", eval_binop "#add_"),
17.95 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
17.96 Calc ("op *", eval_binop "#mult_"),
17.97 Calc ("Atools.pow", eval_binop "#power_")
17.98 ],
18.1 --- a/src/Tools/isac/ProgLang/calculate.sml Thu Sep 23 12:56:51 2010 +0200
18.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Thu Sep 23 14:49:23 2010 +0200
18.3 @@ -137,22 +137,22 @@
18.4 end;
18.5 (*
18.6 > val t = (term_of o the o (parse thy)) "#3 + #4";
18.7 -> val eval_fn = the (assoc (!eval_list, "op +"));
18.8 -> val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
18.9 +> val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus"));
18.10 +> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
18.11 > Syntax.string_of_term (thy2ctxt thy) t';
18.12 > atomty t';
18.13 >
18.14 > val t = (term_of o the o (parse thy)) "(a + #3) + #4";
18.15 -> val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
18.16 +> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
18.17 > Syntax.string_of_term (thy2ctxt thy) t';
18.18 >
18.19 > val t = (term_of o the o (parse thy)) "#3 + (#4 + (a::real))";
18.20 -> val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
18.21 +> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
18.22 > Syntax.string_of_term (thy2ctxt thy) t';
18.23 >
18.24 > val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";
18.25 > atomty t;
18.26 -> val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
18.27 +> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
18.28 > Syntax.string_of_term (thy2ctxt thy) t';
18.29 > val it = "#3 + (#4 + a) = #7 + a" : string
18.30 >
18.31 @@ -273,15 +273,15 @@
18.32 -------------------------------------------------------------------6.8.02:
18.33
18.34 > val ct = (the o (parse thy)) "a+#3+#4";
18.35 -> get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct;
18.36 +> get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
18.37 val it = SOME ("add_3_4","a + 3 + 4 = a + 7 [a + 3 + 4 = a + 7]")
18.38
18.39 > val ct = (the o (parse thy)) "#3+(#4+a)";
18.40 -> get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct;
18.41 +> get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
18.42 val it = SOME ("add_3_4","3 + (4 + a) = 7 + a [3 + (4 + a) = 7 + a]")
18.43
18.44 > val ct = (the o (parse thy)) "a+(#3+#4)+#5";
18.45 -> get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct;
18.46 +> get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
18.47 val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option
18.48
18.49 > val ct = (the o (parse thy)) "#3*(#4*a)";
19.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Thu Sep 23 12:56:51 2010 +0200
19.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Thu Sep 23 14:49:23 2010 +0200
19.3 @@ -389,7 +389,7 @@
19.4 Try $ (Rew_Set $ Free (id_rls rls, IDtype) $ HOLogic.false_const);
19.5 (*val t = rule2stac [] (Thm ("real_diff_minus", num_str @{thm real_diff_minus));
19.6 atomt t; term2str t;
19.7 -val t = rule2stac calclist (Calc ("op +", eval_binop "#add_"));
19.8 +val t = rule2stac calclist (Calc ("Groups.plus_class.plus", eval_binop "#add_"));
19.9 atomt t; term2str t;
19.10 val t = rule2stac [] (Rls_ rearrange_assoc);
19.11 atomt t; term2str t;
19.12 @@ -406,7 +406,7 @@
19.13 HOLogic.false_const);
19.14 (*val t = rule2stac_inst [] (Thm ("real_diff_minus", num_str @{thm real_diff_minus));
19.15 atomt t; term2str t;
19.16 -val t = rule2stac_inst calclist (Calc ("op +", eval_binop "#add_"));
19.17 +val t = rule2stac_inst calclist (Calc ("Groups.plus_class.plus", eval_binop "#add_"));
19.18 atomt t; term2str t;
19.19 val t = rule2stac_inst [] (Rls_ rearrange_assoc);
19.20 atomt t; term2str t;
20.1 --- a/src/Tools/isac/ProgLang/term.sml Thu Sep 23 12:56:51 2010 +0200
20.2 +++ b/src/Tools/isac/ProgLang/term.sml Thu Sep 23 14:49:23 2010 +0200
20.3 @@ -609,10 +609,10 @@
20.4 *)
20.5
20.6 (*used for calculating built in binary operations in Isabelle2002->Float.ML*)
20.7 -(*fun calc "op +" (n1, n2) = n1+n2
20.8 - | calc "op -" (n1, n2) = n1-n2
20.9 +(*fun calc "Groups.plus_class.plus" (n1, n2) = n1+n2
20.10 + | calc "Groups.minus_class.minus" (n1, n2) = n1-n2
20.11 | calc "op *" (n1, n2) = n1*n2
20.12 - | calc "HOL.divide"(n1, n2) = n1 div n2
20.13 + | calc "Rings.inverse_class.divide"(n1, n2) = n1 div n2
20.14 | calc "Atools.pow"(n1, n2) = power n1 n2
20.15 | calc op_ _ = raise error ("calc: operator = "^op_^" not defined");-----*)
20.16 fun calc_equ "op <" (n1, n2) = n1 < n2
20.17 @@ -1163,8 +1163,8 @@
20.18 fun is_atom (Const ("Float.Float",_) $ _) = true
20.19 | is_atom (Const ("ComplexI.I'_'_",_)) = true
20.20 | is_atom (Const ("op *",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t
20.21 - | is_atom (Const ("op +",_) $ t1 $ Const ("ComplexI.I'_'_",_)) = is_atom t1
20.22 - | is_atom (Const ("op +",_) $ t1 $
20.23 + | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ Const ("ComplexI.I'_'_",_)) = is_atom t1
20.24 + | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $
20.25 (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_))) =
20.26 is_atom t1 andalso is_atom t2
20.27 | is_atom (Const _) = true
20.28 @@ -1185,7 +1185,7 @@
20.29 > is_atom t;
20.30 val it = true : bool
20.31 > val t = str2term "1 + 2*I__";
20.32 -> val Const ("op +",_) $ t1 $ (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t;
20.33 +> val Const ("Groups.plus_class.plus",_) $ t1 $ (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t;
20.34 *)
20.35
20.36 (*.adaption from Isabelle/src/Pure/term.ML; reports if ALL Free's
20.37 @@ -1214,6 +1214,6 @@
20.38 let val T1 = type_of t1
20.39 val T2 = type_of t2
20.40 in if T1 <> T2 then raise TYPE ("mk_add gets ",[T1, T2],[t1,t2])
20.41 - else (Const ("op +", [T1, T2] ---> T1) $ t1 $ t2)
20.42 + else (Const ("Groups.plus_class.plus", [T1, T2] ---> T1) $ t1 $ t2)
20.43 end;
20.44
21.1 --- a/test/Tools/isac/Interpret/rewtools.sml Thu Sep 23 12:56:51 2010 +0200
21.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Thu Sep 23 14:49:23 2010 +0200
21.3 @@ -524,10 +524,10 @@
21.4 if contains_rule r1 Test_simplify then ()
21.5 else raise error "rewtools.sml contains_rule Thm";
21.6
21.7 -val r1 = Calc ("op +", eval_binop "#add_");
21.8 +val r1 = Calc ("Groups.plus_class.plus", eval_binop "#add_");
21.9 if contains_rule r1 Test_simplify then ()
21.10 else raise error "rewtools.sml contains_rule Calc";
21.11
21.12 -val r1 = Calc ("op -", eval_binop "#add_");
21.13 +val r1 = Calc ("Groups.minus_class.minus", eval_binop "#add_");
21.14 if not (contains_rule r1 Test_simplify) then ()
21.15 else raise error "rewtools.sml contains_rule Calc";
22.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Thu Sep 23 12:56:51 2010 +0200
22.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Thu Sep 23 14:49:23 2010 +0200
22.3 @@ -142,11 +142,11 @@
22.4 [(*for asm in nth_Cons_ ...*)
22.5 Calc ("op <",eval_equ "#less_"),
22.6 (*2nd nth_Cons_ pushes n+-1 into asms*)
22.7 - Calc("op +", eval_binop "#add_")
22.8 + Calc("Groups.plus_class.plus", eval_binop "#add_")
22.9 ],
22.10 srls = Erls, calc = [],
22.11 rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
22.12 - Calc("op +", eval_binop "#add_"),
22.13 + Calc("Groups.plus_class.plus", eval_binop "#add_"),
22.14 Thm ("nth_Nil_",num_str @{thm nth_Nil_}),
22.15 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
22.16 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
23.1 --- a/test/Tools/isac/Knowledge/diff.sml Thu Sep 23 12:56:51 2010 +0200
23.2 +++ b/test/Tools/isac/Knowledge/diff.sml Thu Sep 23 14:49:23 2010 +0200
23.3 @@ -69,7 +69,7 @@
23.4 Calc ("Atools.occurs'_in", eval_occurs_in ""),
23.5 Calc ("Tools.matches",eval_matches ""),
23.6
23.7 - Calc ("op +",eval_binop "#add_"),
23.8 + Calc ("Groups.plus_class.plus",eval_binop "#add_"),
23.9 Calc ("op *",eval_binop "#mult_"),
23.10 Calc ("Atools.pow" ,eval_binop "#power_"),
23.11
24.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Thu Sep 23 12:56:51 2010 +0200
24.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Thu Sep 23 14:49:23 2010 +0200
24.3 @@ -88,7 +88,7 @@
24.4 val testrls = append_rls "testrls" e_rls
24.5 [(Thm ("length_Nil_",num_str @{thm length_Nil_})),
24.6 (Thm ("length_Cons_",num_str @{thm length_Cons_})),
24.7 - Calc ("op +", eval_binop "#add_"),
24.8 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
24.9 Calc ("op =",eval_equal "#equal_")
24.10 ];
24.11 val SOME (t',_) = rewrite_set_ thy false testrls t;
24.12 @@ -725,7 +725,7 @@
24.13 ##### try calc: op <'
24.14 ### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + -1"]
24.15
24.16 -... i.e Calc ("op +", eval_binop "#add_") was missing in erls_prls_triangular*)
24.17 +... i.e Calc ("Groups.plus_class.plus", eval_binop "#add_") was missing in erls_prls_triangular*)
24.18 trace_rewrite:=false;
24.19 (*WN051014------------------------------------------------------------------*)
24.20
25.1 --- a/test/Tools/isac/Knowledge/integrate.sml Thu Sep 23 12:56:51 2010 +0200
25.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Thu Sep 23 14:49:23 2010 +0200
25.3 @@ -102,7 +102,7 @@
25.4
25.5 val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy;
25.6 "####1###################################################";
25.7 -term2str t' = "x ^^^ 2 * c + c_2 = op + (x ^^^ 2 * c + c_2) c_3" --REDO "op +";
25.8 +term2str t' = "x ^^^ 2 * c + c_2 = op + (x ^^^ 2 * c + c_2) c_3" --REDO "Groups.plus_class.plus";
25.9 "####2###################################################";
25.10
25.11 if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then ()
26.1 --- a/test/Tools/isac/ProgLang/calculate-float.sml Thu Sep 23 12:56:51 2010 +0200
26.2 +++ b/test/Tools/isac/ProgLang/calculate-float.sml Thu Sep 23 14:49:23 2010 +0200
26.3 @@ -38,7 +38,7 @@
26.4 val thy = Float.thy;
26.5
26.6 (*.calculate the value of a pair of floats.*)
26.7 -val ((a,b),(c,d)) = calc "op +" ((~1,0),(0,0)) ((2,0),(0,0));
26.8 +val ((a,b),(c,d)) = calc "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0));
26.9
26.10
26.11 (*.build the term.*)
26.12 @@ -113,7 +113,7 @@
26.13
26.14 (*.the function evaluating a binary operator.*)
26.15 val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0))";
26.16 -val SOME (thmid, t) = eval_binop "#add_" "op +" t thy;
26.17 +val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" t thy;
26.18 term2str t;
26.19
26.20
27.1 --- a/test/Tools/isac/ProgLang/calculate.sml Thu Sep 23 12:56:51 2010 +0200
27.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Thu Sep 23 14:49:23 2010 +0200
27.3 @@ -17,7 +17,7 @@
27.4
27.5 (* [("Vars",("Tools.Vars",fn)),("Length",("Tools.Length",fn)),
27.6 ("Nth",("Tools.Nth",fn)),
27.7 - ("power_",("Atools.pow",fn)),("plus",("op +",fn)),("times",("op *",fn)),
27.8 + ("power_",("Atools.pow",fn)),("plus",("Groups.plus_class.plus",fn)),("times",("op *",fn)),
27.9 ("is_const",("Atools.is'_const",fn)),
27.10 ("le",("op <",fn)),("leq",("op <=",fn)),
27.11 ("ident",("Atools.ident",fn))] *)
27.12 @@ -77,9 +77,9 @@
27.13 ("#Find" ,["realTestFind s_"])
27.14 ],
27.15 {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls,
27.16 - calc=[("plus" ,("op +" ,eval_binop "#add_")),
27.17 + calc=[("plus" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
27.18 ("times" ,("op *" ,eval_binop "#mult_")),
27.19 - ("divide_" ,("HOL.divide" ,eval_cancel "#divide_")),
27.20 + ("divide_" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_")),
27.21 ("power_" ,("Atools.pow" ,eval_binop "#power_"))],
27.22 crls=tval_rls, nrls=e_rls(*,
27.23 asm_rls=[],asm_thm=[]*)},
27.24 @@ -185,7 +185,7 @@
27.25 trace_rewrite:=true;
27.26 val thy = Test.thy;
27.27 val t = (term_of o the o (parse thy)) "(-4) / 2";
27.28 - val SOME (_,t) = eval_cancel "xxx" "HOL.divide" t thy;
27.29 + val SOME (_,t) = eval_cancel "xxx" "Rings.inverse_class.divide" t thy;
27.30 term2str t;
27.31 "-4 / 2 = (-2)";
27.32 (*-------------- but ... *)
28.1 --- a/test/Tools/isac/Test_Isac.thy Thu Sep 23 12:56:51 2010 +0200
28.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Sep 23 14:49:23 2010 +0200
28.3 @@ -81,12 +81,10 @@
28.4 ML {*print_depth 99*}
28.5
28.6 ML {*
28.7 -fun term2str trm = Print_Mode.setmp (Print_Mode.input ::
28.8 - filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ()))
28.9 - (Syntax.string_of_term @{context}) trm;
28.10 -val trm = str2term "a+b"; term2str trm;
28.11 -val trm = str2term "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3"; term2str trm;
28.12 -"=========================================================";
28.13 +str2term "a + b";
28.14 +str2term "a - b";
28.15 +str2term "a * b";
28.16 +str2term "a / b";
28.17 *}
28.18
28.19 use "Knowledge/integrate.sml";