merged
authorhaftmann
Wed Feb 10 08:54:56 2010 +0100 (2010-02-10)
changeset 3508692a8c9ea5aa7
parent 35081 ab02eb4471b3
parent 35085 22bdb7f86a1e
child 35087 e385fa507468
child 35088 6591285a6a59
child 35090 88cc65ae046e
merged
src/HOL/Tools/Nitpick/nitpick_model.ML
     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.4    by (simp add: add_divide_distrib)
     7.5  lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
     7.6    by (simp add: add_divide_distrib)
     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.102  (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
   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