author haftmann Wed Feb 10 08:54:56 2010 +0100 (2010-02-10) changeset 35086 92a8c9ea5aa7 parent 35081 ab02eb4471b3 parent 35085 22bdb7f86a1e child 35087 e385fa507468 child 35088 6591285a6a59 child 35090 88cc65ae046e
merged
```     1.1 --- a/NEWS	Wed Feb 10 00:51:54 2010 +0100
1.2 +++ b/NEWS	Wed Feb 10 08:54:56 2010 +0100
1.3 @@ -20,6 +20,15 @@
1.4  consistent names suitable for name prefixes within the HOL theories.
1.5  INCOMPATIBILITY.
1.6
1.7 +* Some generic constants have been put to appropriate theories:
1.8 +
1.9 +    inverse, divide: Rings
1.10 +
1.11 +INCOMPATIBILITY.
1.12 +
1.13 +* Class division ring also requires proof of fact divide_inverse.  However instantiation
1.14 +of parameter divide has also been required previously.  INCOMPATIBILITY.
1.15 +
1.16  * More consistent naming of type classes involving orderings (and lattices):
1.17
1.18      lower_semilattice                   ~> semilattice_inf
1.19 @@ -76,7 +85,7 @@
1.20
1.21  * New theory Algebras contains generic algebraic structures and
1.22  generic algebraic operations.  INCOMPATIBILTY: constants zero, one,
1.23 -plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and
1.24 +plus, minus, uminus, times, abs, sgn, less_eq and
1.25  less have been moved from HOL.thy to Algebras.thy.
1.26
1.27  * HOLogic.strip_psplit: types are returned in syntactic order, similar
```
```     2.1 --- a/src/HOL/Algebras.thy	Wed Feb 10 00:51:54 2010 +0100
2.2 +++ b/src/HOL/Algebras.thy	Wed Feb 10 08:54:56 2010 +0100
2.3 @@ -103,10 +103,6 @@
2.4  class times =
2.5    fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
2.6
2.7 -class inverse =
2.8 -  fixes inverse :: "'a \<Rightarrow> 'a"
2.9 -    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
2.10 -
2.11  class abs =
2.12    fixes abs :: "'a \<Rightarrow> 'a"
2.13  begin
```
```     3.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Wed Feb 10 00:51:54 2010 +0100
3.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Feb 10 08:54:56 2010 +0100
3.3 @@ -2950,7 +2950,8 @@
3.4                 (\<Sum> i = 0..<Suc n. inverse (real (\<Prod> j \<in> {k..<k+i}. j)) * ?f i (real c) * (xs!x - real c)^i) +
3.5                 inverse (real (\<Prod> j \<in> {k..<k+Suc n}. j)) * ?f (Suc n) t * (xs!x - real c)^Suc n" (is "_ = ?T")
3.6          unfolding funpow_Suc C_def[symmetric] setsum_move0 setprod_head_Suc
3.7 -        by (auto simp add: algebra_simps setsum_right_distrib[symmetric])
3.8 +        by (auto simp add: algebra_simps)
3.9 +          (simp only: mult_left_commute [of _ "inverse (real k)"] setsum_right_distrib [symmetric])
3.10        finally have "?T \<in> {real l .. real u}" . }
3.11      thus ?thesis using DERIV by blast
3.12    qed
```
```     4.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Feb 10 00:51:54 2010 +0100
4.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Feb 10 08:54:56 2010 +0100
4.3 @@ -655,7 +655,7 @@
4.4      if h aconvc y then false else if h aconvc x then true else earlier t x y;
4.5
4.6  fun dest_frac ct = case term_of ct of
4.7 -   Const (@{const_name Algebras.divide},_) \$ a \$ b=>
4.8 +   Const (@{const_name Rings.divide},_) \$ a \$ b=>
4.9      Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
4.10   | Const(@{const_name inverse}, _)\$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
4.11   | t => Rat.rat_of_int (snd (HOLogic.dest_number t))
```
```     5.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 10 00:51:54 2010 +0100
5.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 10 08:54:56 2010 +0100
5.3 @@ -2946,7 +2946,7 @@
5.4  fun num rT x = HOLogic.mk_number rT x;
5.5  fun rrelT rT = [rT,rT] ---> rT;
5.6  fun rrT rT = [rT, rT] ---> bT;
5.7 -fun divt rT = Const(@{const_name Algebras.divide},rrelT rT);
5.8 +fun divt rT = Const(@{const_name Rings.divide},rrelT rT);
5.9  fun timest rT = Const(@{const_name Algebras.times},rrelT rT);
5.10  fun plust rT = Const(@{const_name Algebras.plus},rrelT rT);
5.11  fun minust rT = Const(@{const_name Algebras.minus},rrelT rT);
5.12 @@ -2974,7 +2974,7 @@
5.13   | Const(@{const_name Algebras.minus},_)\$a\$b => @{code poly.Sub} (num_of_term m a, num_of_term m b)
5.14   | Const(@{const_name Algebras.times},_)\$a\$b => @{code poly.Mul} (num_of_term m a, num_of_term m b)
5.15   | Const(@{const_name Power.power},_)\$a\$n => @{code poly.Pw} (num_of_term m a, dest_nat n)
5.16 - | Const(@{const_name Algebras.divide},_)\$a\$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
5.17 + | Const(@{const_name Rings.divide},_)\$a\$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
5.18   | _ => (@{code poly.C} (HOLogic.dest_number t |> snd,1)
5.19           handle TERM _ => @{code poly.Bound} (AList.lookup (op aconv) m t |> the));
5.20
```
```     6.1 --- a/src/HOL/Fields.thy	Wed Feb 10 00:51:54 2010 +0100
6.2 +++ b/src/HOL/Fields.thy	Wed Feb 10 08:54:56 2010 +0100
6.3 @@ -14,8 +14,8 @@
6.4  begin
6.5
6.6  class field = comm_ring_1 + inverse +
6.7 -  assumes field_inverse:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
6.8 -  assumes divide_inverse: "a / b = a * inverse b"
6.9 +  assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
6.10 +  assumes field_divide_inverse: "a / b = a * inverse b"
6.11  begin
6.12
6.13  subclass division_ring
6.14 @@ -24,6 +24,9 @@
6.15    assume "a \<noteq> 0"
6.16    thus "inverse a * a = 1" by (rule field_inverse)
6.17    thus "a * inverse a = 1" by (simp only: mult_commute)
6.18 +next
6.19 +  fix a b :: 'a
6.20 +  show "a / b = a * inverse b" by (rule field_divide_inverse)
6.21  qed
6.22
6.23  subclass idom ..
```
```     7.1 --- a/src/HOL/Groebner_Basis.thy	Wed Feb 10 00:51:54 2010 +0100
7.2 +++ b/src/HOL/Groebner_Basis.thy	Wed Feb 10 08:54:56 2010 +0100
7.3 @@ -489,7 +489,13 @@
7.5  lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
7.7 -ML{* let open Conv in fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute}))))   (@{thm divide_inverse} RS sym)end*}
7.8 +
7.9 +ML {*
7.10 +let open Conv
7.11 +in fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute})))) (@{thm field_divide_inverse} RS sym)
7.12 +end
7.13 +*}
7.14 +
7.15  ML{*
7.16  local
7.17   val zr = @{cpat "0"}
7.18 @@ -527,13 +533,13 @@
7.19      val (l,r) = Thm.dest_binop ct
7.20      val T = ctyp_of_term l
7.21    in (case (term_of l, term_of r) of
7.22 -      (Const(@{const_name Algebras.divide},_)\$_\$_, _) =>
7.23 +      (Const(@{const_name Rings.divide},_)\$_\$_, _) =>
7.24          let val (x,y) = Thm.dest_binop l val z = r
7.25              val _ = map (HOLogic.dest_number o term_of) [x,y,z]
7.26              val ynz = prove_nz ss T y
7.27          in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
7.28          end
7.29 -     | (_, Const (@{const_name Algebras.divide},_)\$_\$_) =>
7.30 +     | (_, Const (@{const_name Rings.divide},_)\$_\$_) =>
7.31          let val (x,y) = Thm.dest_binop r val z = l
7.32              val _ = map (HOLogic.dest_number o term_of) [x,y,z]
7.33              val ynz = prove_nz ss T y
7.34 @@ -543,49 +549,49 @@
7.35    end
7.36    handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
7.37
7.38 - fun is_number (Const(@{const_name Algebras.divide},_)\$a\$b) = is_number a andalso is_number b
7.39 + fun is_number (Const(@{const_name Rings.divide},_)\$a\$b) = is_number a andalso is_number b
7.40     | is_number t = can HOLogic.dest_number t
7.41
7.42   val is_number = is_number o term_of
7.43
7.44   fun proc3 phi ss ct =
7.45    (case term_of ct of
7.46 -    Const(@{const_name Algebras.less},_)\$(Const(@{const_name Algebras.divide},_)\$_\$_)\$_ =>
7.47 +    Const(@{const_name Algebras.less},_)\$(Const(@{const_name Rings.divide},_)\$_\$_)\$_ =>
7.48        let
7.49          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
7.50          val _ = map is_number [a,b,c]
7.51          val T = ctyp_of_term c
7.52          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
7.53        in SOME (mk_meta_eq th) end
7.54 -  | Const(@{const_name Algebras.less_eq},_)\$(Const(@{const_name Algebras.divide},_)\$_\$_)\$_ =>
7.55 +  | Const(@{const_name Algebras.less_eq},_)\$(Const(@{const_name Rings.divide},_)\$_\$_)\$_ =>
7.56        let
7.57          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
7.58          val _ = map is_number [a,b,c]
7.59          val T = ctyp_of_term c
7.60          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
7.61        in SOME (mk_meta_eq th) end
7.62 -  | Const("op =",_)\$(Const(@{const_name Algebras.divide},_)\$_\$_)\$_ =>
7.63 +  | Const("op =",_)\$(Const(@{const_name Rings.divide},_)\$_\$_)\$_ =>
7.64        let
7.65          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
7.66          val _ = map is_number [a,b,c]
7.67          val T = ctyp_of_term c
7.68          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
7.69        in SOME (mk_meta_eq th) end
7.70 -  | Const(@{const_name Algebras.less},_)\$_\$(Const(@{const_name Algebras.divide},_)\$_\$_) =>
7.71 +  | Const(@{const_name Algebras.less},_)\$_\$(Const(@{const_name Rings.divide},_)\$_\$_) =>
7.72      let
7.73        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
7.74          val _ = map is_number [a,b,c]
7.75          val T = ctyp_of_term c
7.76          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
7.77        in SOME (mk_meta_eq th) end
7.78 -  | Const(@{const_name Algebras.less_eq},_)\$_\$(Const(@{const_name Algebras.divide},_)\$_\$_) =>
7.79 +  | Const(@{const_name Algebras.less_eq},_)\$_\$(Const(@{const_name Rings.divide},_)\$_\$_) =>
7.80      let
7.81        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
7.82          val _ = map is_number [a,b,c]
7.83          val T = ctyp_of_term c
7.84          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
7.85        in SOME (mk_meta_eq th) end
7.86 -  | Const("op =",_)\$_\$(Const(@{const_name Algebras.divide},_)\$_\$_) =>
7.87 +  | Const("op =",_)\$_\$(Const(@{const_name Rings.divide},_)\$_\$_) =>
7.88      let
7.89        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
7.90          val _ = map is_number [a,b,c]
7.91 @@ -628,9 +634,9 @@
7.92             @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
7.93             @{thm "diff_def"}, @{thm "minus_divide_left"},
7.94             @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
7.95 -           @{thm divide_inverse} RS sym, @{thm inverse_divide},
7.96 +           @{thm field_divide_inverse} RS sym, @{thm inverse_divide},
7.97             fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute}))))
7.98 -           (@{thm divide_inverse} RS sym)]
7.99 +           (@{thm field_divide_inverse} RS sym)]
7.100
7.101  val comp_conv = (Simplifier.rewrite
7.103 @@ -645,15 +651,15 @@
7.104
7.105  fun numeral_is_const ct =
7.106    case term_of ct of
7.107 -   Const (@{const_name Algebras.divide},_) \$ a \$ b =>
7.108 +   Const (@{const_name Rings.divide},_) \$ a \$ b =>
7.109       can HOLogic.dest_number a andalso can HOLogic.dest_number b
7.110 - | Const (@{const_name Algebras.inverse},_)\$t => can HOLogic.dest_number t
7.111 + | Const (@{const_name Rings.inverse},_)\$t => can HOLogic.dest_number t
7.112   | t => can HOLogic.dest_number t
7.113
7.114  fun dest_const ct = ((case term_of ct of
7.115 -   Const (@{const_name Algebras.divide},_) \$ a \$ b=>
7.116 +   Const (@{const_name Rings.divide},_) \$ a \$ b=>
7.117      Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
7.118 - | Const (@{const_name Algebras.inverse},_)\$t =>
7.119 + | Const (@{const_name Rings.inverse},_)\$t =>
7.120                 Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
7.121   | t => Rat.rat_of_int (snd (HOLogic.dest_number t)))
7.122     handle TERM _ => error "ring_dest_const")
```
```     8.1 --- a/src/HOL/Import/HOL/real.imp	Wed Feb 10 00:51:54 2010 +0100
8.2 +++ b/src/HOL/Import/HOL/real.imp	Wed Feb 10 08:54:56 2010 +0100
8.3 @@ -17,7 +17,7 @@
8.4    "real_ge" > "HOL4Compat.real_ge"
8.5    "pow" > "Power.power_class.power" :: "real => nat => real"
8.6    "abs" > "Algebras.abs" :: "real => real"
8.7 -  "/" > "Algebras.divide" :: "real => real => real"
8.8 +  "/" > "Ring.divide" :: "real => real => real"
8.9
8.10  thm_maps
8.11    "sup_def" > "HOL4Real.real.sup_def"
8.12 @@ -31,7 +31,7 @@
8.13    "real_lt" > "Orderings.linorder_not_le"
8.14    "real_gt" > "HOL4Compat.real_gt"
8.15    "real_ge" > "HOL4Compat.real_ge"
8.16 -  "real_div" > "Rings.field_class.divide_inverse"
8.17 +  "real_div" > "Ring.divide_inverse"
8.18    "pow" > "HOL4Compat.pow"
8.19    "abs" > "HOL4Compat.abs"
8.20    "SUP_LEMMA3" > "HOL4Real.real.SUP_LEMMA3"
```
```     9.1 --- a/src/HOL/Import/HOL/realax.imp	Wed Feb 10 00:51:54 2010 +0100
9.2 +++ b/src/HOL/Import/HOL/realax.imp	Wed Feb 10 08:54:56 2010 +0100
9.3 @@ -33,7 +33,7 @@
9.4    "real_add" > "Algebras.plus_class.plus" :: "real => real => real"
9.5    "real_1" > "Algebras.one_class.one" :: "real"
9.6    "real_0" > "Algebras.zero_class.zero" :: "real"
9.7 -  "inv" > "Algebras.divide_class.inverse" :: "real => real"
9.8 +  "inv" > "Ring.inverse" :: "real => real"
9.9    "hreal_of_treal" > "HOL4Real.realax.hreal_of_treal"
9.10
9.11  thm_maps
```
```    10.1 --- a/src/HOL/NSA/StarDef.thy	Wed Feb 10 00:51:54 2010 +0100
10.2 +++ b/src/HOL/NSA/StarDef.thy	Wed Feb 10 08:54:56 2010 +0100
10.3 @@ -893,6 +893,7 @@
10.4  apply (intro_classes)
10.5  apply (transfer, erule left_inverse)
10.6  apply (transfer, erule right_inverse)
10.7 +apply (transfer, fact divide_inverse)
10.8  done
10.9
10.10  instance star :: (field) field
```
```    11.1 --- a/src/HOL/Rings.thy	Wed Feb 10 00:51:54 2010 +0100
11.2 +++ b/src/HOL/Rings.thy	Wed Feb 10 08:54:56 2010 +0100
11.3 @@ -410,9 +410,14 @@
11.4
11.5  end
11.6
11.7 +class inverse =
11.8 +  fixes inverse :: "'a \<Rightarrow> 'a"
11.9 +    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
11.10 +
11.11  class division_ring = ring_1 + inverse +
11.12    assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
11.13    assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
11.14 +  assumes divide_inverse: "a / b = a * inverse b"
11.15  begin
11.16
11.17  subclass ring_1_no_zero_divisors
```
```    12.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Feb 10 00:51:54 2010 +0100
12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Feb 10 08:54:56 2010 +0100
12.3 @@ -88,7 +88,7 @@
12.4      Const (nth_atom_name pool "" T j k, T)
12.5
12.6  (* term -> real *)
12.7 -fun extract_real_number (Const (@{const_name Algebras.divide}, _) \$ t1 \$ t2) =
12.8 +fun extract_real_number (Const (@{const_name Rings.divide}, _) \$ t1 \$ t2) =
12.9      real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
12.10    | extract_real_number t = real (snd (HOLogic.dest_number t))
12.11  (* term * term -> order *)
12.12 @@ -459,7 +459,7 @@
12.13                             0 => mk_num 0
12.14                           | n1 => case HOLogic.dest_number t2 |> snd of
12.15                                     1 => mk_num n1
12.16 -                                 | n2 => Const (@{const_name Algebras.divide},
12.17 +                                 | n2 => Const (@{const_name Rings.divide},
12.18                                                  num_T --> num_T --> num_T)
12.19                                           \$ mk_num n1 \$ mk_num n2)
12.20                        | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
```
```    13.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Feb 10 00:51:54 2010 +0100
13.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Feb 10 08:54:56 2010 +0100
13.3 @@ -150,7 +150,7 @@
13.4                (SOME t', m'') => (SOME (mC \$ s' \$ t'), m'')
13.5              | (NONE,    m'') => (SOME s', m''))
13.6          | (NONE,    m') => demult (t, m')))
13.7 -    | demult ((mC as Const (@{const_name Algebras.divide}, _)) \$ s \$ t, m) =
13.8 +    | demult ((mC as Const (@{const_name Rings.divide}, _)) \$ s \$ t, m) =
13.9        (* FIXME: Shouldn't we simplify nested quotients, e.g. '(s/t)/u' could
13.10           become 's/(t*u)', and '(s*t)/u' could become 's*(t/u)' ?   Note that
13.11           if we choose to do so here, the simpset used by arith must be able to
13.12 @@ -212,7 +212,7 @@
13.13          (case demult inj_consts (all, m) of
13.14             (NONE,   m') => (p, Rat.add i m')
13.15           | (SOME u, m') => add_atom u m' pi)
13.16 -    | poly (all as Const (@{const_name Algebras.divide}, _) \$ _ \$ _, m, pi as (p, i)) =
13.17 +    | poly (all as Const (@{const_name Rings.divide}, _) \$ _ \$ _, m, pi as (p, i)) =
13.18          (case demult inj_consts (all, m) of
13.19             (NONE,   m') => (p, Rat.add i m')
13.20           | (SOME u, m') => add_atom u m' pi)
```
```    14.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Wed Feb 10 00:51:54 2010 +0100
14.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Wed Feb 10 08:54:56 2010 +0100
14.3 @@ -96,7 +96,7 @@
14.4    Fractions are reduced later by the cancel_numeral_factor simproc.*)
14.5  fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
14.6
14.7 -val mk_divide = HOLogic.mk_binop @{const_name Algebras.divide};
14.8 +val mk_divide = HOLogic.mk_binop @{const_name Rings.divide};
14.9
14.10  (*Build term (p / q) * t*)
14.11  fun mk_fcoeff ((p, q), t) =
14.12 @@ -105,7 +105,7 @@
14.13
14.14  (*Express t as a product of a fraction with other sorted terms*)
14.15  fun dest_fcoeff sign (Const (@{const_name Algebras.uminus}, _) \$ t) = dest_fcoeff (~sign) t
14.16 -  | dest_fcoeff sign (Const (@{const_name Algebras.divide}, _) \$ t \$ u) =
14.17 +  | dest_fcoeff sign (Const (@{const_name Rings.divide}, _) \$ t \$ u) =
14.18      let val (p, t') = dest_coeff sign t
14.19          val (q, u') = dest_coeff 1 u
14.20      in (mk_frac (p, q), mk_divide (t', u')) end
14.21 @@ -391,8 +391,8 @@
14.22  structure DivideCancelNumeralFactor = CancelNumeralFactorFun
14.23   (open CancelNumeralFactorCommon
14.24    val prove_conv = Arith_Data.prove_conv
14.25 -  val mk_bal   = HOLogic.mk_binop @{const_name Algebras.divide}
14.26 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT
14.27 +  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
14.28 +  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} Term.dummyT
14.29    val cancel = @{thm mult_divide_mult_cancel_left} RS trans
14.30    val neg_exchanges = false
14.31  )
14.32 @@ -570,8 +570,8 @@
14.33  structure DivideCancelFactor = ExtractCommonTermFun
14.34   (open CancelFactorCommon
14.35    val prove_conv = Arith_Data.prove_conv
14.36 -  val mk_bal   = HOLogic.mk_binop @{const_name Algebras.divide}
14.37 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT
14.38 +  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
14.39 +  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} Term.dummyT
14.40    fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
14.41  );
14.42
```
```    15.1 --- a/src/HOL/ex/SVC_Oracle.thy	Wed Feb 10 00:51:54 2010 +0100
15.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Wed Feb 10 08:54:56 2010 +0100
15.3 @@ -65,7 +65,7 @@
15.4      (*abstraction of a real/rational expression*)
15.5      fun rat ((c as Const(@{const_name Algebras.plus}, _)) \$ x \$ y) = c \$ (rat x) \$ (rat y)
15.6        | rat ((c as Const(@{const_name Algebras.minus}, _)) \$ x \$ y) = c \$ (rat x) \$ (rat y)
15.7 -      | rat ((c as Const(@{const_name Algebras.divide}, _)) \$ x \$ y) = c \$ (rat x) \$ (rat y)
15.8 +      | rat ((c as Const(@{const_name Rings.divide}, _)) \$ x \$ y) = c \$ (rat x) \$ (rat y)
15.9        | rat ((c as Const(@{const_name Algebras.times}, _)) \$ x \$ y) = c \$ (rat x) \$ (rat y)
15.10        | rat ((c as Const(@{const_name Algebras.uminus}, _)) \$ x) = c \$ (rat x)
15.11        | rat t = lit t
```
```    16.1 --- a/src/HOL/ex/svc_funcs.ML	Wed Feb 10 00:51:54 2010 +0100
16.2 +++ b/src/HOL/ex/svc_funcs.ML	Wed Feb 10 08:54:56 2010 +0100
16.3 @@ -173,7 +173,7 @@
16.4        | tm (Const(@{const_name Algebras.times}, T) \$ x \$ y) =
16.5            if is_numeric_op T then Interp("*", [tm x, tm y])
16.6            else fail t
16.7 -      | tm (Const(@{const_name Algebras.inverse}, T) \$ x) =
16.8 +      | tm (Const(@{const_name Rings.inverse}, T) \$ x) =
16.9            if domain_type T = HOLogic.realT then
16.10                Rat(1, litExp x)
16.11            else fail t
```