1.1 --- a/src/Tools/isac/Knowledge/Atools.thy Thu Feb 08 13:20:40 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Fri Feb 09 11:16:05 2018 +0100
1.3 @@ -256,7 +256,7 @@
1.4 val (T1, _, _) = dest_binop_typ t0
1.5 val res =
1.6 calcul (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0)n1 n2
1.7 - (*WN071229 "Fields.inverse_class.divide" never tried*)
1.8 + (*WN071229 "Rings.divide_class.divide" never tried*)
1.9 val rhs = var_op_float v op_ t0 T1 res
1.10 val prop = Trueprop $ (mk_equality (t, rhs))
1.11 in SOME ("#: " ^ term2str prop, prop) end
1.12 @@ -420,8 +420,8 @@
1.13 (** evaluation on the metalevel **)
1.14
1.15 (*. evaluate HOL.divide .*)
1.16 -(*("DIVIDE" ,("Fields.inverse_class.divide" ,eval_cancel "#divide_e"))*)
1.17 -fun eval_cancel (thmid:string) "Fields.inverse_class.divide" (t as
1.18 +(*("DIVIDE" ,("Rings.divide_class.divide" ,eval_cancel "#divide_e"))*)
1.19 +fun eval_cancel (thmid:string) "Rings.divide_class.divide" (t as
1.20 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
1.21 (case (int_of_str n1, int_of_str n2) of
1.22 (SOME n1', SOME n2') =>
1.23 @@ -682,7 +682,7 @@
1.24 ("PLUS" ,("Groups.plus_class.plus", eval_binop "#add_")),
1.25 ("MINUS" ,("Groups.minus_class.minus", eval_binop "#sub_")),
1.26 ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")),
1.27 - ("DIVIDE" ,("Fields.inverse_class.divide", eval_cancel "#divide_e")),
1.28 + ("DIVIDE" ,("Rings.divide_class.divide", eval_cancel "#divide_e")),
1.29 ("POWER" ,("Atools.pow", eval_binop "#power_")),
1.30 ("boollist2sum",("Atools.boollist2sum", eval_boollist2sum ""))] *}
1.31 ML {*
2.1 --- a/src/Tools/isac/Knowledge/Delete.thy Thu Feb 08 13:20:40 2018 +0100
2.2 +++ b/src/Tools/isac/Knowledge/Delete.thy Fri Feb 09 11:16:05 2018 +0100
2.3 @@ -29,7 +29,7 @@
2.4 ((a - c,0),(0,0))
2.5 | calcul "Groups.times_class.times" ((a, b), _) ((c, d), _) = (*FIXXXME precision*)
2.6 ((a * c, b + d), (0, 0))
2.7 - | calcul "Fields.inverse_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
2.8 + | calcul "Rings.divide_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
2.9 ((a div c, 0), (0, 0))
2.10 | calcul "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*)
2.11 ((power a c, 0), (0, 0))
3.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Thu Feb 08 13:20:40 2018 +0100
3.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Fri Feb 09 11:16:05 2018 +0100
3.3 @@ -263,7 +263,7 @@
3.4 (*Rls_ discard_parentheses *3**),
3.5 Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
3.6 Rls_ separate_bdv2,
3.7 - Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e")
3.8 + Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
3.9 ],
3.10 scr = EmptyScr}:rls;
3.11 *}
3.12 @@ -281,7 +281,7 @@
3.13 Rls_ discard_parentheses,
3.14 Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
3.15 Rls_ separate_bdv2,
3.16 - Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e")
3.17 + Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
3.18 ],
3.19 scr = EmptyScr}:rls;
3.20 (*
4.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Thu Feb 08 13:20:40 2018 +0100
4.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Fri Feb 09 11:16:05 2018 +0100
4.3 @@ -197,7 +197,7 @@
4.4 Thm ("divide_divide_eq_left",
4.5 num_str @{thm divide_divide_eq_left}),
4.6 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
4.7 - Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e"),
4.8 + Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e"),
4.9
4.10 Thm ("rat_power", num_str @{thm rat_power})
4.11 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
4.12 @@ -261,7 +261,7 @@
4.13 Rls_ discard_parentheses,
4.14 (*Rls_ collect_bdv, from make_polynomial_in*)
4.15 Rls_ separate_bdv2,
4.16 - Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e")
4.17 + Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
4.18 ],
4.19 scr = EmptyScr}:rls;
4.20
4.21 @@ -299,7 +299,7 @@
4.22 * num_str @{thm add_divide_distrib})
4.23 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
4.24 * ]),
4.25 -* Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e")
4.26 +* Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
4.27 * ],
4.28 * scr = EmptyScr
4.29 * }:rls);
5.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Thu Feb 08 13:20:40 2018 +0100
5.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Fri Feb 09 11:16:05 2018 +0100
5.3 @@ -54,7 +54,7 @@
5.4 [Thm ("real_assoc_1",num_str @{thm real_assoc_1})
5.5 (*
5.6 Don't use
5.7 - Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
5.8 + Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
5.9 Calc ("Atools.pow" ,eval_binop "#power_"),
5.10 *)
5.11 ];
5.12 @@ -65,7 +65,7 @@
5.13 [Thm ("real_assoc_1",num_str @{thm real_assoc_1})
5.14 (*
5.15 Don't use
5.16 - Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
5.17 + Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
5.18 Calc ("Atools.pow" ,eval_binop "#power_"),
5.19 *)
5.20 ];
5.21 @@ -86,7 +86,7 @@
5.22 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
5.23 Calc ("Groups.times_class.times",eval_binop "#mult_"),
5.24 (* Dont use
5.25 - Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
5.26 + Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
5.27 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
5.28 *)
5.29 Calc ("Atools.pow" ,eval_binop "#power_")
6.1 --- a/src/Tools/isac/Knowledge/Poly.thy Thu Feb 08 13:20:40 2018 +0100
6.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Fri Feb 09 11:16:05 2018 +0100
6.3 @@ -176,7 +176,7 @@
6.4 let fun coeff_in c v = member op = (vars c) v;
6.5 fun finddivide (_ $ _ $ _ $ _) v = error("is_polyrat_in:")
6.6 (* at the moment there is no term like this, but ....*)
6.7 - | finddivide (t as (Const ("Fields.inverse_class.divide",_) $ _ $ b)) v =
6.8 + | finddivide (t as (Const ("Rings.divide_class.divide",_) $ _ $ b)) v =
6.9 not(coeff_in b v)
6.10 | finddivide (_ $ t1 $ t2) v =
6.11 (finddivide t1 v) orelse (finddivide t2 v)
6.12 @@ -1336,7 +1336,7 @@
6.13 eval_is_multUnordered "")],
6.14 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
6.15 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
6.16 - ("DIVIDE", ("Fields.inverse_class.divide",
6.17 + ("DIVIDE", ("Rings.divide_class.divide",
6.18 eval_cancel "#divide_e")),
6.19 ("POWER" , ("Atools.pow", eval_binop "#power_"))],
6.20 errpatts = [],
6.21 @@ -1390,7 +1390,7 @@
6.22 eval_is_addUnordered "")],
6.23 calc = [("PLUS" ,("Groups.plus_class.plus", eval_binop "#add_")),
6.24 ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")),
6.25 - ("DIVIDE",("Fields.inverse_class.divide",
6.26 + ("DIVIDE",("Rings.divide_class.divide",
6.27 eval_cancel "#divide_e")),
6.28 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
6.29 errpatts = [],
7.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Thu Feb 08 13:20:40 2018 +0100
7.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Fri Feb 09 11:16:05 2018 +0100
7.3 @@ -470,7 +470,7 @@
7.4 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
7.5 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
7.6 Calc ("Groups.times_class.times",eval_binop "#mult_"),
7.7 - Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
7.8 + Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
7.9 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
7.10 Calc ("Atools.pow" ,eval_binop "#power_"),
7.11 Rls_ reduce_012
7.12 @@ -1331,7 +1331,7 @@
7.13 Rls_ separate_bdvs,
7.14 (* Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*)
7.15 Rls_ cancel_p
7.16 - (*Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e") too weak!*)
7.17 + (*Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e") too weak!*)
7.18 ],
7.19 scr = EmptyScr}:rls);
7.20 *}
8.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Thu Feb 08 13:20:40 2018 +0100
8.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Fri Feb 09 11:16:05 2018 +0100
8.3 @@ -63,7 +63,7 @@
8.4 fun coeff_in c v = member op = (vars c) v;
8.5 fun finddivide (_ $ _ $ _ $ _) v = error("is_rateqation_in:")
8.6 (* at the moment there is no term like this, but ....*)
8.7 - | finddivide (t as (Const ("Fields.inverse_class.divide",_) $ _ $ b)) v = coeff_in b v
8.8 + | finddivide (t as (Const ("Rings.divide_class.divide",_) $ _ $ b)) v = coeff_in b v
8.9 | finddivide (_ $ t1 $ t2) v = (finddivide t1 v)
8.10 orelse (finddivide t2 v)
8.11 | finddivide (_ $ t1) v = (finddivide t1 v)
8.12 @@ -105,7 +105,7 @@
8.13 (merge_rls "is_ratequation_in" calculate_Rational
8.14 (append_rls "is_ratequation_in"
8.15 Poly_erls
8.16 - [(*Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),*)
8.17 + [(*Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),*)
8.18 Calc ("RatEq.is'_ratequation'_in",
8.19 eval_is_ratequation_in "")
8.20
8.21 @@ -122,7 +122,7 @@
8.22 (merge_rls "is_ratequation_in" calculate_Rational
8.23 (append_rls "is_ratequation_in"
8.24 Poly_erls
8.25 - [(*Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),*)
8.26 + [(*Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),*)
8.27 Calc ("RatEq.is'_ratequation'_in",
8.28 eval_is_ratequation_in "")
8.29 ]))
9.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Feb 08 13:20:40 2018 +0100
9.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Fri Feb 09 11:16:05 2018 +0100
9.3 @@ -26,7 +26,7 @@
9.4 | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
9.5 | is_ratpolyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
9.6 | is_ratpolyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
9.7 - | is_ratpolyexp (Const ("Fields.inverse_class.divide",_) $ Free _ $ Free _) = true
9.8 + | is_ratpolyexp (Const ("Rings.divide_class.divide",_) $ Free _ $ Free _) = true
9.9 | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
9.10 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
9.11 | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
9.12 @@ -35,7 +35,7 @@
9.13 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
9.14 | is_ratpolyexp (Const ("Atools.pow",_) $ t1 $ t2) =
9.15 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
9.16 - | is_ratpolyexp (Const ("Fields.inverse_class.divide",_) $ t1 $ t2) =
9.17 + | is_ratpolyexp (Const ("Rings.divide_class.divide",_) $ t1 $ t2) =
9.18 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
9.19 | is_ratpolyexp _ = false;
9.20
9.21 @@ -52,7 +52,7 @@
9.22 (*("get_denominator", ("Rational.get_denominator", eval_get_denominator ""))*)
9.23 fun eval_get_denominator (thmid:string) _
9.24 (t as Const ("Rational.get_denominator", _) $
9.25 - (Const ("Fields.inverse_class.divide", _) $ num $
9.26 + (Const ("Rings.divide_class.divide", _) $ num $
9.27 denom)) thy =
9.28 SOME (mk_thmid thmid "" (term_to_string''' thy denom) "",
9.29 Trueprop $ (mk_equality (t, denom)))
9.30 @@ -61,7 +61,7 @@
9.31 (*("get_numerator", ("Rational.get_numerator", eval_get_numerator ""))*)
9.32 fun eval_get_numerator (thmid:string) _
9.33 (t as Const ("Rational.get_numerator", _) $
9.34 - (Const ("Fields.inverse_class.divide", _) $num
9.35 + (Const ("Rings.divide_class.divide", _) $num
9.36 $denom )) thy =
9.37 SOME (mk_thmid thmid "" (term_to_string''' thy num) "",
9.38 Trueprop $ (mk_equality (t, num)))
9.39 @@ -212,7 +212,7 @@
9.40 subsubsection {* Factor out gcd for cancellation *}
9.41 ML {*
9.42 fun check_fraction t =
9.43 - let val Const ("Fields.inverse_class.divide", _) $ numerator $ denominator = t
9.44 + let val Const ("Rings.divide_class.divide", _) $ numerator $ denominator = t
9.45 in SOME (numerator, denominator) end
9.46 handle Bind => NONE
9.47
9.48 @@ -243,7 +243,7 @@
9.49 val b't = term_of_poly baseT expT vs b'
9.50 val ct = term_of_poly baseT expT vs c
9.51 val t' =
9.52 - HOLogic.mk_binop "Fields.inverse_class.divide"
9.53 + HOLogic.mk_binop "Rings.divide_class.divide"
9.54 (HOLogic.mk_binop "Groups.times_class.times"
9.55 (term_of_poly baseT expT vs a', ct),
9.56 HOLogic.mk_binop "Groups.times_class.times" (b't, ct))
9.57 @@ -289,7 +289,7 @@
9.58 val bt' = term_of_poly baseT expT vs b'
9.59 val ct = term_of_poly baseT expT vs c
9.60 val t' =
9.61 - HOLogic.mk_binop "Fields.inverse_class.divide"
9.62 + HOLogic.mk_binop "Rings.divide_class.divide"
9.63 (term_of_poly baseT expT vs a', bt')
9.64 val asm = mk_asms baseT [bt']
9.65 in SOME (t', asm) end
9.66 @@ -304,17 +304,17 @@
9.67 (* addition of fractions allows (at most) one non-fraction (a monomial) *)
9.68 fun check_frac_sum
9.69 (Const ("Groups.plus_class.plus", _) $
9.70 - (Const ("Fields.inverse_class.divide", _) $ n1 $ d1) $
9.71 - (Const ("Fields.inverse_class.divide", _) $ n2 $ d2))
9.72 + (Const ("Rings.divide_class.divide", _) $ n1 $ d1) $
9.73 + (Const ("Rings.divide_class.divide", _) $ n2 $ d2))
9.74 = SOME ((n1, d1), (n2, d2))
9.75 | check_frac_sum
9.76 (Const ("Groups.plus_class.plus", _) $
9.77 nofrac $
9.78 - (Const ("Fields.inverse_class.divide", _) $ n2 $ d2))
9.79 + (Const ("Rings.divide_class.divide", _) $ n2 $ d2))
9.80 = SOME ((nofrac, Free ("1", HOLogic.realT)), (n2, d2))
9.81 | check_frac_sum
9.82 (Const ("Groups.plus_class.plus", _) $
9.83 - (Const ("Fields.inverse_class.divide", _) $ n1 $ d1) $
9.84 + (Const ("Rings.divide_class.divide", _) $ n1 $ d1) $
9.85 nofrac)
9.86 = SOME ((n1, d1), (nofrac, Free ("1", HOLogic.realT)))
9.87 | check_frac_sum _ = NONE
9.88 @@ -348,9 +348,9 @@
9.89 HOLogic.mk_binop "Groups.times_class.times" (d1', d2')) (*--------------*)
9.90 val t' =
9.91 HOLogic.mk_binop "Groups.plus_class.plus"
9.92 - (HOLogic.mk_binop "Fields.inverse_class.divide"
9.93 + (HOLogic.mk_binop "Rings.divide_class.divide"
9.94 (HOLogic.mk_binop "Groups.times_class.times" (n1, d2'), denom),
9.95 - HOLogic.mk_binop "Fields.inverse_class.divide"
9.96 + HOLogic.mk_binop "Rings.divide_class.divide"
9.97 (HOLogic.mk_binop "Groups.times_class.times" (n2, d1'), denom))
9.98 val asm = mk_asms baseT [d1', d2', c']
9.99 in SOME (t', asm) end
9.100 @@ -381,7 +381,7 @@
9.101 val nomin = term_of_poly baseT expT vs
9.102 (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'))
9.103 val denom = term_of_poly baseT expT vs ((c %%*%% a') %%*%% b')
9.104 - val t' = HOLogic.mk_binop "Fields.inverse_class.divide" (nomin, denom)
9.105 + val t' = HOLogic.mk_binop "Rings.divide_class.divide" (nomin, denom)
9.106 in SOME (t', mk_asms baseT [denom]) end
9.107 | _ => NONE : (term * term list) option
9.108 end
9.109 @@ -412,7 +412,7 @@
9.110 erls = calc_rat_erls, srls = Erls,
9.111 calc = [], errpatts = [],
9.112 rules =
9.113 - [Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
9.114 + [Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
9.115
9.116 Thm ("minus_divide_left", num_str (@{thm minus_divide_left} RS @{thm sym})),
9.117 (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
9.118 @@ -518,7 +518,7 @@
9.119 calc =
9.120 [("PLUS", ("Groups.plus_class.plus", eval_binop "#add_")),
9.121 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
9.122 - ("DIVIDE", ("Fields.inverse_class.divide", eval_cancel "#divide_e")),
9.123 + ("DIVIDE", ("Rings.divide_class.divide", eval_cancel "#divide_e")),
9.124 ("POWER", ("Atools.pow", eval_binop "#power_"))],
9.125 errpatts = [],
9.126 scr =
9.127 @@ -585,7 +585,7 @@
9.128 erls = rational_erls,
9.129 calc = [("PLUS", ("Groups.plus_class.plus", eval_binop "#add_")),
9.130 ("TIMES", ("Groups.times_class.times", eval_binop "#mult_")),
9.131 - ("DIVIDE", ("Fields.inverse_class.divide", eval_cancel "#divide_e")),
9.132 + ("DIVIDE", ("Rings.divide_class.divide", eval_cancel "#divide_e")),
9.133 ("POWER", ("Atools.pow", eval_binop "#power_"))],
9.134 errpatts = [],
9.135 scr = Rfuns {init_state = init_state thy Atools_erls ro,
9.136 @@ -674,7 +674,7 @@
9.137 Thm ("divide_divide_eq_left",
9.138 num_str @{thm divide_divide_eq_left}),
9.139 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
9.140 - Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e")
9.141 + Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
9.142 ],
9.143 scr = EmptyScr
9.144 }:rls);
9.145 @@ -816,7 +816,7 @@
9.146 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
9.147 Thm ("divide_divide_eq_left", num_str @{thm divide_divide_eq_left}),
9.148 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
9.149 - Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
9.150 + Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
9.151
9.152 Thm ("rat_power", num_str @{thm rat_power})
9.153 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
10.1 --- a/src/Tools/isac/Knowledge/Root.thy Thu Feb 08 13:20:40 2018 +0100
10.2 +++ b/src/Tools/isac/Knowledge/Root.thy Fri Feb 09 11:16:05 2018 +0100
10.3 @@ -165,7 +165,7 @@
10.4 append_rls "Root_crls" Atools_erls
10.5 [Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
10.6 Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"),
10.7 - Calc ("Fields.inverse_class.divide",eval_cancel "#divide_e"),
10.8 + Calc ("Rings.divide_class.divide",eval_cancel "#divide_e"),
10.9 Calc ("Atools.pow" ,eval_binop "#power_"),
10.10 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
10.11 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
10.12 @@ -177,7 +177,7 @@
10.13 append_rls "Root_erls" Atools_erls
10.14 [Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
10.15 Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"),
10.16 - Calc ("Fields.inverse_class.divide",eval_cancel "#divide_e"),
10.17 + Calc ("Rings.divide_class.divide",eval_cancel "#divide_e"),
10.18 Calc ("Atools.pow" ,eval_binop "#power_"),
10.19 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
10.20 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
10.21 @@ -295,7 +295,7 @@
10.22 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
10.23 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
10.24 Calc ("Groups.times_class.times", eval_binop "#mult_"),
10.25 - Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e"),
10.26 + Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e"),
10.27 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
10.28 Calc ("Atools.pow", eval_binop "#power_"),
10.29
10.30 @@ -320,7 +320,7 @@
10.31 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
10.32 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
10.33 Calc ("Groups.times_class.times", eval_binop "#mult_"),
10.34 - Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e"),
10.35 + Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e"),
10.36 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
10.37 Calc ("Atools.pow", eval_binop "#power_")
10.38 ],
11.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Thu Feb 08 13:20:40 2018 +0100
11.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Fri Feb 09 11:16:05 2018 +0100
11.3 @@ -165,7 +165,7 @@
11.4 | isnorm (Const ("Groups.plus_class.plus",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
11.5 | isnorm (Const ("Groups.times_class.times",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
11.6 | isnorm (Const ("Groups.minus_class.minus",_) $ _ $ _) v = false
11.7 - | isnorm (Const ("Fields.inverse_class.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse
11.8 + | isnorm (Const ("Rings.divide_class.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse
11.9 (is_sqrtTerm_in t2 v)
11.10 | isnorm (Const ("NthRoot.sqrt",_) $ t1) v = coeff_in t1 v
11.11 | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v
11.12 @@ -453,7 +453,7 @@
11.13 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
11.14 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
11.15 Calc ("Groups.times_class.times",eval_binop "#mult_"),
11.16 - Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
11.17 + Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
11.18 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
11.19 Calc ("Atools.pow" ,eval_binop "#power_"),
11.20 Thm("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),
12.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Thu Feb 08 13:20:40 2018 +0100
12.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Fri Feb 09 11:16:05 2018 +0100
12.3 @@ -55,7 +55,7 @@
12.4 | rootadd _ _ = false;
12.5 fun findrootrat (_ $ _ $ _ $ _) v = error("is_rootRatAddTerm_in:")
12.6 (* at the moment there is no term like this, but ....*)
12.7 - | findrootrat (t as (Const ("Fields.inverse_class.divide",_) $ _ $ t3)) v =
12.8 + | findrootrat (t as (Const ("Rings.divide_class.divide",_) $ _ $ t3)) v =
12.9 if (is_rootTerm_in t3 v) then rootadd t3 v else false
12.10 | findrootrat (_ $ t1 $ t2) v =
12.11 (findrootrat t1 v) orelse (findrootrat t2 v)
13.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Feb 08 13:20:40 2018 +0100
13.2 +++ b/src/Tools/isac/Knowledge/Test.thy Fri Feb 09 11:16:05 2018 +0100
13.3 @@ -403,7 +403,7 @@
13.4 thus they MUST be done IMMEDIATELY before calc *)
13.5 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
13.6 Calc ("Groups.times_class.times", eval_binop "#mult_"),
13.7 - Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
13.8 + Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
13.9 Calc ("Atools.pow", eval_binop "#power_"),
13.10
13.11 Thm ("rcollect_right",num_str @{thm rcollect_right}),
13.12 @@ -481,7 +481,7 @@
13.13 (*aus Atools.ML*)
13.14 ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
13.15 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
13.16 - ("DIVIDE" ,("Fields.inverse_class.divide" ,eval_cancel "#divide_e")),
13.17 + ("DIVIDE" ,("Rings.divide_class.divide" ,eval_cancel "#divide_e")),
13.18 ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
13.19 ("is_const",("Atools.is'_const",eval_const "#is_const_")),
13.20 ("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),
14.1 --- a/src/Tools/isac/ProgLang/termC.sml Thu Feb 08 13:20:40 2018 +0100
14.2 +++ b/src/Tools/isac/ProgLang/termC.sml Fri Feb 09 11:16:05 2018 +0100
14.3 @@ -677,7 +677,7 @@
14.4 (*fun calc "Groups.plus_class.plus" (n1, n2) = n1+n2
14.5 | calc "Groups.minus_class.minus" (n1, n2) = n1-n2
14.6 | calc "Groups.times_class.times" (n1, n2) = n1*n2
14.7 - | calc "Fields.inverse_class.divide"(n1, n2) = n1 div n2
14.8 + | calc "Rings.divide_class.divide"(n1, n2) = n1 div n2
14.9 | calc "Atools.pow"(n1, n2) = power n1 n2
14.10 | calc op_ _ = error ("calc: operator = "^op_^" not defined");-----*)
14.11 fun calc_equ "less" (n1, n2) = n1 < n2
15.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Thu Feb 08 13:20:40 2018 +0100
15.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Fri Feb 09 11:16:05 2018 +0100
15.3 @@ -24,7 +24,7 @@
15.4 *)
15.5 fun eval_get_denominator (thmid:string) _
15.6 (t as Const ("Rational.get_denominator", _) $
15.7 - (Const ("Fields.inverse_class.divide", _) $num
15.8 + (Const ("Rings.divide_class.divide", _) $num
15.9 $denom)) thy =
15.10 SOME (mk_thmid thmid "" (term_to_string''' thy denom) "",
15.11 Trueprop $ (mk_equality (t, denom)))
16.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Feb 08 13:20:40 2018 +0100
16.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri Feb 09 11:16:05 2018 +0100
16.3 @@ -182,7 +182,7 @@
16.4 ML {*
16.5 val (_, expr) = HOLogic.dest_eq fun3'; term2str expr;
16.6 val (_, denom) =
16.7 - HOLogic.dest_bin "Fields.inverse_class.divide" (type_of expr) expr;
16.8 + HOLogic.dest_bin "Rings.divide_class.divide" (type_of expr) expr;
16.9 term2str denom = "-1 + -2 * z + 8 * z ^^^ 2";
16.10 *}
16.11
16.12 @@ -216,7 +216,7 @@
16.13 *)
16.14 fun eval_get_denominator (thmid:string) _
16.15 (t as Const ("Rational.get_denominator", _) $
16.16 - (Const ("Fields.inverse_class.divide", _) $num
16.17 + (Const ("Rings.divide_class.divide", _) $num
16.18 $denom)) thy =
16.19 SOME (mk_thmid thmid "" (term_to_string''' thy denom) "",
16.20 Trueprop $ (mk_equality (t, denom)))
16.21 @@ -236,7 +236,7 @@
16.22 *)
16.23 fun eval_get_numerator (thmid:string) _
16.24 (t as Const ("Rational.get_numerator", _) $
16.25 - (Const ("Fields.inverse_class.divide", _) $num
16.26 + (Const ("Rings.divide_class.divide", _) $num
16.27 $denom )) thy =
16.28 SOME (mk_thmid thmid "" (term_to_string''' thy num) "",
16.29 Trueprop $ (mk_equality (t, num)))
16.30 @@ -589,7 +589,7 @@
16.31 val SOME numerator = parseNEW ctxt "3::real";
16.32
16.33 val expr' = HOLogic.mk_binop
16.34 - "Fields.inverse_class.divide" (numerator, denominator');
16.35 + "Rings.divide_class.divide" (numerator, denominator');
16.36 term2str expr';
16.37 *}
16.38
17.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Thu Feb 08 13:20:40 2018 +0100
17.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Fri Feb 09 11:16:05 2018 +0100
17.3 @@ -91,8 +91,8 @@
17.4 val denom2 = parseNEW ctxt "(z + -1 * (-1 / 4))::real" |> the;
17.5
17.6 val test = HOLogic.mk_binop "Groups.plus_class.plus"
17.7 - (HOLogic.mk_binop "Fields.inverse_class.divide" (A_var, denom1),
17.8 - HOLogic.mk_binop "Fields.inverse_class.divide" (B_var, denom2));
17.9 + (HOLogic.mk_binop "Rings.divide_class.divide" (A_var, denom1),
17.10 + HOLogic.mk_binop "Rings.divide_class.divide" (B_var, denom2));
17.11
17.12 if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))" then ()
17.13 else error "HOLogic.mk_binop broken ?";
18.1 --- a/test/Tools/isac/ProgLang/calculate.sml Thu Feb 08 13:20:40 2018 +0100
18.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Fri Feb 09 11:16:05 2018 +0100
18.3 @@ -13,7 +13,6 @@
18.4 "----------- fun norm -----------------------------------";
18.5 "----------- check return value of adhoc_thm ----";
18.6 "----------- fun calculate_ -----------------------------";
18.7 -"----------- fun calculate_ -----------------------------";
18.8 "----------- calculate from script --requires 'setup'----";
18.9 "----------- calculate check test-root-equ --------------";
18.10 "----------- check calcul,ate bottom up -----------------";
18.11 @@ -163,7 +162,7 @@
18.12 val thy = @{theory Test};
18.13 val t = (Thm.term_of o the o (parse thy)) "(-4) / 2";
18.14
18.15 -val SOME (_, t) = eval_cancel "xxx" "Fields.inverse_class.divide" t thy;
18.16 +val SOME (_, t) = eval_cancel "xxx" "Rings.divide_class.divide" t thy;
18.17
18.18 term2str t;
18.19 "-4 / 2 = (-2)";