--- a/NEWS Wed Feb 10 08:49:26 2010 +0100
+++ b/NEWS Wed Feb 10 08:49:26 2010 +0100
@@ -20,6 +20,15 @@
consistent names suitable for name prefixes within the HOL theories.
INCOMPATIBILITY.
+* Some generic constants have been put to appropriate theories:
+
+ inverse, divide: Rings
+
+INCOMPATIBILITY.
+
+* Class division ring also requires proof of fact divide_inverse. However instantiation
+of parameter divide has also been required previously. INCOMPATIBILITY.
+
* More consistent naming of type classes involving orderings (and lattices):
lower_semilattice ~> semilattice_inf
@@ -76,7 +85,7 @@
* New theory Algebras contains generic algebraic structures and
generic algebraic operations. INCOMPATIBILTY: constants zero, one,
-plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and
+plus, minus, uminus, times, abs, sgn, less_eq and
less have been moved from HOL.thy to Algebras.thy.
* HOLogic.strip_psplit: types are returned in syntactic order, similar
--- a/src/HOL/Algebras.thy Wed Feb 10 08:49:26 2010 +0100
+++ b/src/HOL/Algebras.thy Wed Feb 10 08:49:26 2010 +0100
@@ -103,10 +103,6 @@
class times =
fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
-class inverse =
- fixes inverse :: "'a \<Rightarrow> 'a"
- and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70)
-
class abs =
fixes abs :: "'a \<Rightarrow> 'a"
begin
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Feb 10 08:49:26 2010 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Feb 10 08:49:26 2010 +0100
@@ -655,7 +655,7 @@
if h aconvc y then false else if h aconvc x then true else earlier t x y;
fun dest_frac ct = case term_of ct of
- Const (@{const_name Algebras.divide},_) $ a $ b=>
+ Const (@{const_name Rings.divide},_) $ a $ b=>
Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
| Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
| t => Rat.rat_of_int (snd (HOLogic.dest_number t))
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Feb 10 08:49:26 2010 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Feb 10 08:49:26 2010 +0100
@@ -2946,7 +2946,7 @@
fun num rT x = HOLogic.mk_number rT x;
fun rrelT rT = [rT,rT] ---> rT;
fun rrT rT = [rT, rT] ---> bT;
-fun divt rT = Const(@{const_name Algebras.divide},rrelT rT);
+fun divt rT = Const(@{const_name Rings.divide},rrelT rT);
fun timest rT = Const(@{const_name Algebras.times},rrelT rT);
fun plust rT = Const(@{const_name Algebras.plus},rrelT rT);
fun minust rT = Const(@{const_name Algebras.minus},rrelT rT);
@@ -2974,7 +2974,7 @@
| Const(@{const_name Algebras.minus},_)$a$b => @{code poly.Sub} (num_of_term m a, num_of_term m b)
| Const(@{const_name Algebras.times},_)$a$b => @{code poly.Mul} (num_of_term m a, num_of_term m b)
| Const(@{const_name Power.power},_)$a$n => @{code poly.Pw} (num_of_term m a, dest_nat n)
- | Const(@{const_name Algebras.divide},_)$a$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
+ | Const(@{const_name Rings.divide},_)$a$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
| _ => (@{code poly.C} (HOLogic.dest_number t |> snd,1)
handle TERM _ => @{code poly.Bound} (AList.lookup (op aconv) m t |> the));
--- a/src/HOL/Fields.thy Wed Feb 10 08:49:26 2010 +0100
+++ b/src/HOL/Fields.thy Wed Feb 10 08:49:26 2010 +0100
@@ -14,8 +14,8 @@
begin
class field = comm_ring_1 + inverse +
- assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
- assumes divide_inverse: "a / b = a * inverse b"
+ assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
+ assumes field_divide_inverse: "a / b = a * inverse b"
begin
subclass division_ring
@@ -24,6 +24,9 @@
assume "a \<noteq> 0"
thus "inverse a * a = 1" by (rule field_inverse)
thus "a * inverse a = 1" by (simp only: mult_commute)
+next
+ fix a b :: 'a
+ show "a / b = a * inverse b" by (rule field_divide_inverse)
qed
subclass idom ..
--- a/src/HOL/Groebner_Basis.thy Wed Feb 10 08:49:26 2010 +0100
+++ b/src/HOL/Groebner_Basis.thy Wed Feb 10 08:49:26 2010 +0100
@@ -489,7 +489,13 @@
by (simp add: add_divide_distrib)
lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
by (simp add: add_divide_distrib)
-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*}
+
+ML {*
+let open Conv
+in fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute})))) (@{thm field_divide_inverse} RS sym)
+end
+*}
+
ML{*
local
val zr = @{cpat "0"}
@@ -527,13 +533,13 @@
val (l,r) = Thm.dest_binop ct
val T = ctyp_of_term l
in (case (term_of l, term_of r) of
- (Const(@{const_name Algebras.divide},_)$_$_, _) =>
+ (Const(@{const_name Rings.divide},_)$_$_, _) =>
let val (x,y) = Thm.dest_binop l val z = r
val _ = map (HOLogic.dest_number o term_of) [x,y,z]
val ynz = prove_nz ss T y
in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
end
- | (_, Const (@{const_name Algebras.divide},_)$_$_) =>
+ | (_, Const (@{const_name Rings.divide},_)$_$_) =>
let val (x,y) = Thm.dest_binop r val z = l
val _ = map (HOLogic.dest_number o term_of) [x,y,z]
val ynz = prove_nz ss T y
@@ -543,49 +549,49 @@
end
handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
- fun is_number (Const(@{const_name Algebras.divide},_)$a$b) = is_number a andalso is_number b
+ fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b
| is_number t = can HOLogic.dest_number t
val is_number = is_number o term_of
fun proc3 phi ss ct =
(case term_of ct of
- Const(@{const_name Algebras.less},_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
+ Const(@{const_name Algebras.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name Algebras.less_eq},_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
+ | Const(@{const_name Algebras.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
in SOME (mk_meta_eq th) end
- | Const("op =",_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
+ | Const("op =",_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name Algebras.less},_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
+ | Const(@{const_name Algebras.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name Algebras.less_eq},_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
+ | Const(@{const_name Algebras.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
in SOME (mk_meta_eq th) end
- | Const("op =",_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
+ | Const("op =",_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
@@ -628,9 +634,9 @@
@{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
@{thm "diff_def"}, @{thm "minus_divide_left"},
@{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
- @{thm divide_inverse} RS sym, @{thm inverse_divide},
+ @{thm field_divide_inverse} RS sym, @{thm inverse_divide},
fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute}))))
- (@{thm divide_inverse} RS sym)]
+ (@{thm field_divide_inverse} RS sym)]
val comp_conv = (Simplifier.rewrite
(HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
@@ -645,15 +651,15 @@
fun numeral_is_const ct =
case term_of ct of
- Const (@{const_name Algebras.divide},_) $ a $ b =>
+ Const (@{const_name Rings.divide},_) $ a $ b =>
can HOLogic.dest_number a andalso can HOLogic.dest_number b
- | Const (@{const_name Algebras.inverse},_)$t => can HOLogic.dest_number t
+ | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t
| t => can HOLogic.dest_number t
fun dest_const ct = ((case term_of ct of
- Const (@{const_name Algebras.divide},_) $ a $ b=>
+ Const (@{const_name Rings.divide},_) $ a $ b=>
Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
- | Const (@{const_name Algebras.inverse},_)$t =>
+ | Const (@{const_name Rings.inverse},_)$t =>
Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
| t => Rat.rat_of_int (snd (HOLogic.dest_number t)))
handle TERM _ => error "ring_dest_const")
--- a/src/HOL/Import/HOL/realax.imp Wed Feb 10 08:49:26 2010 +0100
+++ b/src/HOL/Import/HOL/realax.imp Wed Feb 10 08:49:26 2010 +0100
@@ -33,7 +33,7 @@
"real_add" > "Algebras.plus_class.plus" :: "real => real => real"
"real_1" > "Algebras.one_class.one" :: "real"
"real_0" > "Algebras.zero_class.zero" :: "real"
- "inv" > "Algebras.divide_class.inverse" :: "real => real"
+ "inv" > "Ring.inverse" :: "real => real"
"hreal_of_treal" > "HOL4Real.realax.hreal_of_treal"
thm_maps
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Feb 10 08:49:26 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Feb 10 08:49:26 2010 +0100
@@ -78,7 +78,7 @@
Const (atom_name "" T j, T)
(* term -> real *)
-fun extract_real_number (Const (@{const_name Algebras.divide}, _) $ t1 $ t2) =
+fun extract_real_number (Const (@{const_name Rings.divide}, _) $ t1 $ t2) =
real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
| extract_real_number t = real (snd (HOLogic.dest_number t))
(* term * term -> order *)
@@ -446,7 +446,7 @@
0 => mk_num 0
| n1 => case HOLogic.dest_number t2 |> snd of
1 => mk_num n1
- | n2 => Const (@{const_name Algebras.divide},
+ | n2 => Const (@{const_name Rings.divide},
num_T --> num_T --> num_T)
$ mk_num n1 $ mk_num n2)
| _ => raise TERM ("Nitpick_Model.reconstruct_term.\
--- a/src/HOL/Tools/lin_arith.ML Wed Feb 10 08:49:26 2010 +0100
+++ b/src/HOL/Tools/lin_arith.ML Wed Feb 10 08:49:26 2010 +0100
@@ -150,7 +150,7 @@
(SOME t', m'') => (SOME (mC $ s' $ t'), m'')
| (NONE, m'') => (SOME s', m''))
| (NONE, m') => demult (t, m')))
- | demult ((mC as Const (@{const_name Algebras.divide}, _)) $ s $ t, m) =
+ | demult ((mC as Const (@{const_name Rings.divide}, _)) $ s $ t, m) =
(* FIXME: Shouldn't we simplify nested quotients, e.g. '(s/t)/u' could
become 's/(t*u)', and '(s*t)/u' could become 's*(t/u)' ? Note that
if we choose to do so here, the simpset used by arith must be able to
@@ -212,7 +212,7 @@
(case demult inj_consts (all, m) of
(NONE, m') => (p, Rat.add i m')
| (SOME u, m') => add_atom u m' pi)
- | poly (all as Const (@{const_name Algebras.divide}, _) $ _ $ _, m, pi as (p, i)) =
+ | poly (all as Const (@{const_name Rings.divide}, _) $ _ $ _, m, pi as (p, i)) =
(case demult inj_consts (all, m) of
(NONE, m') => (p, Rat.add i m')
| (SOME u, m') => add_atom u m' pi)
--- a/src/HOL/Tools/numeral_simprocs.ML Wed Feb 10 08:49:26 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Wed Feb 10 08:49:26 2010 +0100
@@ -96,7 +96,7 @@
Fractions are reduced later by the cancel_numeral_factor simproc.*)
fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
-val mk_divide = HOLogic.mk_binop @{const_name Algebras.divide};
+val mk_divide = HOLogic.mk_binop @{const_name Rings.divide};
(*Build term (p / q) * t*)
fun mk_fcoeff ((p, q), t) =
@@ -105,7 +105,7 @@
(*Express t as a product of a fraction with other sorted terms*)
fun dest_fcoeff sign (Const (@{const_name Algebras.uminus}, _) $ t) = dest_fcoeff (~sign) t
- | dest_fcoeff sign (Const (@{const_name Algebras.divide}, _) $ t $ u) =
+ | dest_fcoeff sign (Const (@{const_name Rings.divide}, _) $ t $ u) =
let val (p, t') = dest_coeff sign t
val (q, u') = dest_coeff 1 u
in (mk_frac (p, q), mk_divide (t', u')) end
@@ -391,8 +391,8 @@
structure DivideCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binop @{const_name Algebras.divide}
- val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT
+ val mk_bal = HOLogic.mk_binop @{const_name Rings.divide}
+ val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} Term.dummyT
val cancel = @{thm mult_divide_mult_cancel_left} RS trans
val neg_exchanges = false
)
@@ -570,8 +570,8 @@
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binop @{const_name Algebras.divide}
- val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT
+ val mk_bal = HOLogic.mk_binop @{const_name Rings.divide}
+ val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} Term.dummyT
fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
);
--- a/src/HOL/ex/SVC_Oracle.thy Wed Feb 10 08:49:26 2010 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy Wed Feb 10 08:49:26 2010 +0100
@@ -65,7 +65,7 @@
(*abstraction of a real/rational expression*)
fun rat ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
| rat ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
- | rat ((c as Const(@{const_name Algebras.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+ | rat ((c as Const(@{const_name Rings.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
| rat ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
| rat ((c as Const(@{const_name Algebras.uminus}, _)) $ x) = c $ (rat x)
| rat t = lit t
--- a/src/HOL/ex/svc_funcs.ML Wed Feb 10 08:49:26 2010 +0100
+++ b/src/HOL/ex/svc_funcs.ML Wed Feb 10 08:49:26 2010 +0100
@@ -173,7 +173,7 @@
| tm (Const(@{const_name Algebras.times}, T) $ x $ y) =
if is_numeric_op T then Interp("*", [tm x, tm y])
else fail t
- | tm (Const(@{const_name Algebras.inverse}, T) $ x) =
+ | tm (Const(@{const_name Rings.inverse}, T) $ x) =
if domain_type T = HOLogic.realT then
Rat(1, litExp x)
else fail t