# HG changeset patch # User huffman # Date 1312822329 25200 # Node ID 5bce8ff0d9aeef8c637f997c88c2f510e3ed38ed # Parent 4588597ba37e90d5d127bda445b643172359bfc5 moved division ring stuff from Rings.thy to Fields.thy diff -r 4588597ba37e -r 5bce8ff0d9ae src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Aug 08 08:55:49 2011 -0700 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Aug 08 09:52:09 2011 -0700 @@ -652,7 +652,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 Rings.divide},_) $ a $ b=> + Const (@{const_name Fields.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)) diff -r 4588597ba37e -r 5bce8ff0d9ae src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Aug 08 08:55:49 2011 -0700 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Aug 08 09:52:09 2011 -0700 @@ -2856,7 +2856,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 Rings.divide},rrelT rT); +fun divt rT = Const(@{const_name Fields.divide},rrelT rT); fun timest rT = Const(@{const_name Groups.times},rrelT rT); fun plust rT = Const(@{const_name Groups.plus},rrelT rT); fun minust rT = Const(@{const_name Groups.minus},rrelT rT); @@ -2884,7 +2884,7 @@ | Const(@{const_name Groups.minus},_)$a$b => @{code poly.Sub} (num_of_term m a, num_of_term m b) | Const(@{const_name Groups.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 Rings.divide},_)$a$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd) + | Const(@{const_name Fields.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)); diff -r 4588597ba37e -r 5bce8ff0d9ae src/HOL/Fields.thy --- a/src/HOL/Fields.thy Mon Aug 08 08:55:49 2011 -0700 +++ b/src/HOL/Fields.thy Mon Aug 08 09:52:09 2011 -0700 @@ -13,6 +13,225 @@ imports Rings begin +subsection {* Division rings *} + +text {* + A division ring is like a field, but without the commutativity requirement. +*} + +class inverse = + fixes inverse :: "'a \ 'a" + and divide :: "'a \ 'a \ 'a" (infixl "'/" 70) + +class division_ring = ring_1 + inverse + + assumes left_inverse [simp]: "a \ 0 \ inverse a * a = 1" + assumes right_inverse [simp]: "a \ 0 \ a * inverse a = 1" + assumes divide_inverse: "a / b = a * inverse b" +begin + +subclass ring_1_no_zero_divisors +proof + fix a b :: 'a + assume a: "a \ 0" and b: "b \ 0" + show "a * b \ 0" + proof + assume ab: "a * b = 0" + hence "0 = inverse a * (a * b) * inverse b" by simp + also have "\ = (inverse a * a) * (b * inverse b)" + by (simp only: mult_assoc) + also have "\ = 1" using a b by simp + finally show False by simp + qed +qed + +lemma nonzero_imp_inverse_nonzero: + "a \ 0 \ inverse a \ 0" +proof + assume ianz: "inverse a = 0" + assume "a \ 0" + hence "1 = a * inverse a" by simp + also have "... = 0" by (simp add: ianz) + finally have "1 = 0" . + thus False by (simp add: eq_commute) +qed + +lemma inverse_zero_imp_zero: + "inverse a = 0 \ a = 0" +apply (rule classical) +apply (drule nonzero_imp_inverse_nonzero) +apply auto +done + +lemma inverse_unique: + assumes ab: "a * b = 1" + shows "inverse a = b" +proof - + have "a \ 0" using ab by (cases "a = 0") simp_all + moreover have "inverse a * (a * b) = inverse a" by (simp add: ab) + ultimately show ?thesis by (simp add: mult_assoc [symmetric]) +qed + +lemma nonzero_inverse_minus_eq: + "a \ 0 \ inverse (- a) = - inverse a" +by (rule inverse_unique) simp + +lemma nonzero_inverse_inverse_eq: + "a \ 0 \ inverse (inverse a) = a" +by (rule inverse_unique) simp + +lemma nonzero_inverse_eq_imp_eq: + assumes "inverse a = inverse b" and "a \ 0" and "b \ 0" + shows "a = b" +proof - + from `inverse a = inverse b` + have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong) + with `a \ 0` and `b \ 0` show "a = b" + by (simp add: nonzero_inverse_inverse_eq) +qed + +lemma inverse_1 [simp]: "inverse 1 = 1" +by (rule inverse_unique) simp + +lemma nonzero_inverse_mult_distrib: + assumes "a \ 0" and "b \ 0" + shows "inverse (a * b) = inverse b * inverse a" +proof - + have "a * (b * inverse b) * inverse a = 1" using assms by simp + hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult_assoc) + thus ?thesis by (rule inverse_unique) +qed + +lemma division_ring_inverse_add: + "a \ 0 \ b \ 0 \ inverse a + inverse b = inverse a * (a + b) * inverse b" +by (simp add: algebra_simps) + +lemma division_ring_inverse_diff: + "a \ 0 \ b \ 0 \ inverse a - inverse b = inverse a * (b - a) * inverse b" +by (simp add: algebra_simps) + +lemma right_inverse_eq: "b \ 0 \ a / b = 1 \ a = b" +proof + assume neq: "b \ 0" + { + hence "a = (a / b) * b" by (simp add: divide_inverse mult_assoc) + also assume "a / b = 1" + finally show "a = b" by simp + next + assume "a = b" + with neq show "a / b = 1" by (simp add: divide_inverse) + } +qed + +lemma nonzero_inverse_eq_divide: "a \ 0 \ inverse a = 1 / a" +by (simp add: divide_inverse) + +lemma divide_self [simp]: "a \ 0 \ a / a = 1" +by (simp add: divide_inverse) + +lemma divide_zero_left [simp]: "0 / a = 0" +by (simp add: divide_inverse) + +lemma inverse_eq_divide: "inverse a = 1 / a" +by (simp add: divide_inverse) + +lemma add_divide_distrib: "(a+b) / c = a/c + b/c" +by (simp add: divide_inverse algebra_simps) + +lemma divide_1 [simp]: "a / 1 = a" + by (simp add: divide_inverse) + +lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c" + by (simp add: divide_inverse mult_assoc) + +lemma minus_divide_left: "- (a / b) = (-a) / b" + by (simp add: divide_inverse) + +lemma nonzero_minus_divide_right: "b \ 0 ==> - (a / b) = a / (- b)" + by (simp add: divide_inverse nonzero_inverse_minus_eq) + +lemma nonzero_minus_divide_divide: "b \ 0 ==> (-a) / (-b) = a / b" + by (simp add: divide_inverse nonzero_inverse_minus_eq) + +lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)" + by (simp add: divide_inverse) + +lemma diff_divide_distrib: "(a - b) / c = a / c - b / c" + by (simp add: diff_minus add_divide_distrib) + +lemma nonzero_eq_divide_eq [field_simps]: "c \ 0 \ a = b / c \ a * c = b" +proof - + assume [simp]: "c \ 0" + have "a = b / c \ a * c = (b / c) * c" by simp + also have "... \ a * c = b" by (simp add: divide_inverse mult_assoc) + finally show ?thesis . +qed + +lemma nonzero_divide_eq_eq [field_simps]: "c \ 0 \ b / c = a \ b = a * c" +proof - + assume [simp]: "c \ 0" + have "b / c = a \ (b / c) * c = a * c" by simp + also have "... \ b = a * c" by (simp add: divide_inverse mult_assoc) + finally show ?thesis . +qed + +lemma divide_eq_imp: "c \ 0 \ b = a * c \ b / c = a" + by (simp add: divide_inverse mult_assoc) + +lemma eq_divide_imp: "c \ 0 \ a * c = b \ a = b / c" + by (drule sym) (simp add: divide_inverse mult_assoc) + +end + +class division_ring_inverse_zero = division_ring + + assumes inverse_zero [simp]: "inverse 0 = 0" +begin + +lemma divide_zero [simp]: + "a / 0 = 0" + by (simp add: divide_inverse) + +lemma divide_self_if [simp]: + "a / a = (if a = 0 then 0 else 1)" + by simp + +lemma inverse_nonzero_iff_nonzero [simp]: + "inverse a = 0 \ a = 0" + by rule (fact inverse_zero_imp_zero, simp) + +lemma inverse_minus_eq [simp]: + "inverse (- a) = - inverse a" +proof cases + assume "a=0" thus ?thesis by simp +next + assume "a\0" + thus ?thesis by (simp add: nonzero_inverse_minus_eq) +qed + +lemma inverse_eq_imp_eq: + "inverse a = inverse b \ a = b" +apply (cases "a=0 | b=0") + apply (force dest!: inverse_zero_imp_zero + simp add: eq_commute [of "0::'a"]) +apply (force dest!: nonzero_inverse_eq_imp_eq) +done + +lemma inverse_eq_iff_eq [simp]: + "inverse a = inverse b \ a = b" + by (force dest!: inverse_eq_imp_eq) + +lemma inverse_inverse_eq [simp]: + "inverse (inverse a) = a" +proof cases + assume "a=0" thus ?thesis by simp +next + assume "a\0" + thus ?thesis by (simp add: nonzero_inverse_inverse_eq) +qed + +end + +subsection {* Fields *} + class field = comm_ring_1 + inverse + assumes field_inverse: "a \ 0 \ inverse a * a = 1" assumes field_divide_inverse: "a / b = a * inverse b" @@ -249,7 +468,7 @@ end -text {* Ordered Fields *} +subsection {* Ordered fields *} class linordered_field = field + linordered_idom begin diff -r 4588597ba37e -r 5bce8ff0d9ae src/HOL/Import/Generate-HOL/GenHOL4Real.thy --- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Mon Aug 08 08:55:49 2011 -0700 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Mon Aug 08 09:52:09 2011 -0700 @@ -52,7 +52,7 @@ real_ge > HOL4Compat.real_ge real_lte > Orderings.less_eq :: "[real,real] => bool" real_sub > Groups.minus :: "[real,real] => real" - "/" > Rings.divide :: "[real,real] => real" + "/" > Fields.divide :: "[real,real] => real" pow > Power.power :: "[real,nat] => real" abs > Groups.abs :: "real => real" real_of_num > RealDef.real :: "nat => real"; diff -r 4588597ba37e -r 5bce8ff0d9ae src/HOL/Import/Generate-HOLLight/GenHOLLight.thy --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Mon Aug 08 08:55:49 2011 -0700 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Mon Aug 08 09:52:09 2011 -0700 @@ -162,11 +162,11 @@ MEASURE > HOLLightCompat.MEASURE (*real_of_num > RealDef.real :: "nat => real" real_neg > Groups.uminus_class.uminus :: "real => real" - real_inv > Rings.inverse_class.inverse :: "real => real" + real_inv > Fields.inverse_class.inverse :: "real => real" real_add > Groups.plus_class.plus :: "real => real => real" real_sub > Groups.minus_class.minus :: "real => real => real" real_mul > Groups.times_class.times :: "real => real => real" - real_div > Rings.inverse_class.divide :: "real => real => real" + real_div > Fields.inverse_class.divide :: "real => real => real" real_lt > Orderings.ord_class.less :: "real \ real \ bool" real_le > Orderings.ord_class.less_eq :: "real \ real \ bool" real_gt > Orderings.ord_class.greater :: "real \ real \ bool" diff -r 4588597ba37e -r 5bce8ff0d9ae src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Aug 08 08:55:49 2011 -0700 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Aug 08 09:52:09 2011 -0700 @@ -285,7 +285,7 @@ (@{const_name "Groups.plus_class.plus"}, @{typ "prop => prop => prop"}), (@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}), (@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}), - (@{const_name "Rings.inverse_class.divide"}, @{typ "prop => prop => prop"}), + (@{const_name "Fields.inverse_class.divide"}, @{typ "prop => prop => prop"}), (@{const_name "Lattices.semilattice_inf_class.inf"}, @{typ "prop => prop => prop"}), (@{const_name "Lattices.semilattice_sup_class.sup"}, @{typ "prop => prop => prop"}), (@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}), diff -r 4588597ba37e -r 5bce8ff0d9ae src/HOL/Rings.thy --- a/src/HOL/Rings.thy Mon Aug 08 08:55:49 2011 -0700 +++ b/src/HOL/Rings.thy Mon Aug 08 09:52:09 2011 -0700 @@ -417,217 +417,6 @@ end -class inverse = - fixes inverse :: "'a \ 'a" - and divide :: "'a \ 'a \ 'a" (infixl "'/" 70) - -class division_ring = ring_1 + inverse + - assumes left_inverse [simp]: "a \ 0 \ inverse a * a = 1" - assumes right_inverse [simp]: "a \ 0 \ a * inverse a = 1" - assumes divide_inverse: "a / b = a * inverse b" -begin - -subclass ring_1_no_zero_divisors -proof - fix a b :: 'a - assume a: "a \ 0" and b: "b \ 0" - show "a * b \ 0" - proof - assume ab: "a * b = 0" - hence "0 = inverse a * (a * b) * inverse b" by simp - also have "\ = (inverse a * a) * (b * inverse b)" - by (simp only: mult_assoc) - also have "\ = 1" using a b by simp - finally show False by simp - qed -qed - -lemma nonzero_imp_inverse_nonzero: - "a \ 0 \ inverse a \ 0" -proof - assume ianz: "inverse a = 0" - assume "a \ 0" - hence "1 = a * inverse a" by simp - also have "... = 0" by (simp add: ianz) - finally have "1 = 0" . - thus False by (simp add: eq_commute) -qed - -lemma inverse_zero_imp_zero: - "inverse a = 0 \ a = 0" -apply (rule classical) -apply (drule nonzero_imp_inverse_nonzero) -apply auto -done - -lemma inverse_unique: - assumes ab: "a * b = 1" - shows "inverse a = b" -proof - - have "a \ 0" using ab by (cases "a = 0") simp_all - moreover have "inverse a * (a * b) = inverse a" by (simp add: ab) - ultimately show ?thesis by (simp add: mult_assoc [symmetric]) -qed - -lemma nonzero_inverse_minus_eq: - "a \ 0 \ inverse (- a) = - inverse a" -by (rule inverse_unique) simp - -lemma nonzero_inverse_inverse_eq: - "a \ 0 \ inverse (inverse a) = a" -by (rule inverse_unique) simp - -lemma nonzero_inverse_eq_imp_eq: - assumes "inverse a = inverse b" and "a \ 0" and "b \ 0" - shows "a = b" -proof - - from `inverse a = inverse b` - have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong) - with `a \ 0` and `b \ 0` show "a = b" - by (simp add: nonzero_inverse_inverse_eq) -qed - -lemma inverse_1 [simp]: "inverse 1 = 1" -by (rule inverse_unique) simp - -lemma nonzero_inverse_mult_distrib: - assumes "a \ 0" and "b \ 0" - shows "inverse (a * b) = inverse b * inverse a" -proof - - have "a * (b * inverse b) * inverse a = 1" using assms by simp - hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult_assoc) - thus ?thesis by (rule inverse_unique) -qed - -lemma division_ring_inverse_add: - "a \ 0 \ b \ 0 \ inverse a + inverse b = inverse a * (a + b) * inverse b" -by (simp add: algebra_simps) - -lemma division_ring_inverse_diff: - "a \ 0 \ b \ 0 \ inverse a - inverse b = inverse a * (b - a) * inverse b" -by (simp add: algebra_simps) - -lemma right_inverse_eq: "b \ 0 \ a / b = 1 \ a = b" -proof - assume neq: "b \ 0" - { - hence "a = (a / b) * b" by (simp add: divide_inverse mult_assoc) - also assume "a / b = 1" - finally show "a = b" by simp - next - assume "a = b" - with neq show "a / b = 1" by (simp add: divide_inverse) - } -qed - -lemma nonzero_inverse_eq_divide: "a \ 0 \ inverse a = 1 / a" -by (simp add: divide_inverse) - -lemma divide_self [simp]: "a \ 0 \ a / a = 1" -by (simp add: divide_inverse) - -lemma divide_zero_left [simp]: "0 / a = 0" -by (simp add: divide_inverse) - -lemma inverse_eq_divide: "inverse a = 1 / a" -by (simp add: divide_inverse) - -lemma add_divide_distrib: "(a+b) / c = a/c + b/c" -by (simp add: divide_inverse algebra_simps) - -lemma divide_1 [simp]: "a / 1 = a" - by (simp add: divide_inverse) - -lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c" - by (simp add: divide_inverse mult_assoc) - -lemma minus_divide_left: "- (a / b) = (-a) / b" - by (simp add: divide_inverse) - -lemma nonzero_minus_divide_right: "b \ 0 ==> - (a / b) = a / (- b)" - by (simp add: divide_inverse nonzero_inverse_minus_eq) - -lemma nonzero_minus_divide_divide: "b \ 0 ==> (-a) / (-b) = a / b" - by (simp add: divide_inverse nonzero_inverse_minus_eq) - -lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)" - by (simp add: divide_inverse) - -lemma diff_divide_distrib: "(a - b) / c = a / c - b / c" - by (simp add: diff_minus add_divide_distrib) - -lemma nonzero_eq_divide_eq [field_simps]: "c \ 0 \ a = b / c \ a * c = b" -proof - - assume [simp]: "c \ 0" - have "a = b / c \ a * c = (b / c) * c" by simp - also have "... \ a * c = b" by (simp add: divide_inverse mult_assoc) - finally show ?thesis . -qed - -lemma nonzero_divide_eq_eq [field_simps]: "c \ 0 \ b / c = a \ b = a * c" -proof - - assume [simp]: "c \ 0" - have "b / c = a \ (b / c) * c = a * c" by simp - also have "... \ b = a * c" by (simp add: divide_inverse mult_assoc) - finally show ?thesis . -qed - -lemma divide_eq_imp: "c \ 0 \ b = a * c \ b / c = a" - by (simp add: divide_inverse mult_assoc) - -lemma eq_divide_imp: "c \ 0 \ a * c = b \ a = b / c" - by (drule sym) (simp add: divide_inverse mult_assoc) - -end - -class division_ring_inverse_zero = division_ring + - assumes inverse_zero [simp]: "inverse 0 = 0" -begin - -lemma divide_zero [simp]: - "a / 0 = 0" - by (simp add: divide_inverse) - -lemma divide_self_if [simp]: - "a / a = (if a = 0 then 0 else 1)" - by simp - -lemma inverse_nonzero_iff_nonzero [simp]: - "inverse a = 0 \ a = 0" - by rule (fact inverse_zero_imp_zero, simp) - -lemma inverse_minus_eq [simp]: - "inverse (- a) = - inverse a" -proof cases - assume "a=0" thus ?thesis by simp -next - assume "a\0" - thus ?thesis by (simp add: nonzero_inverse_minus_eq) -qed - -lemma inverse_eq_imp_eq: - "inverse a = inverse b \ a = b" -apply (cases "a=0 | b=0") - apply (force dest!: inverse_zero_imp_zero - simp add: eq_commute [of "0::'a"]) -apply (force dest!: nonzero_inverse_eq_imp_eq) -done - -lemma inverse_eq_iff_eq [simp]: - "inverse a = inverse b \ a = b" - by (force dest!: inverse_eq_imp_eq) - -lemma inverse_inverse_eq [simp]: - "inverse (inverse a) = a" -proof cases - assume "a=0" thus ?thesis by simp -next - assume "a\0" - thus ?thesis by (simp add: nonzero_inverse_inverse_eq) -qed - -end - text {* The theory of partially ordered rings is taken from the books: \begin{itemize} diff -r 4588597ba37e -r 5bce8ff0d9ae src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Mon Aug 08 08:55:49 2011 -0700 +++ b/src/HOL/Tools/lin_arith.ML Mon Aug 08 09:52:09 2011 -0700 @@ -151,7 +151,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 Rings.divide}, _)) $ s $ t, m) = + | demult ((mC as Const (@{const_name Fields.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 @@ -213,7 +213,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 Rings.divide}, _) $ _ $ _, m, pi as (p, i)) = + | poly (all as Const (@{const_name Fields.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) diff -r 4588597ba37e -r 5bce8ff0d9ae src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Mon Aug 08 08:55:49 2011 -0700 +++ b/src/HOL/Tools/numeral_simprocs.ML Mon Aug 08 09:52:09 2011 -0700 @@ -97,7 +97,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 Rings.divide}; +val mk_divide = HOLogic.mk_binop @{const_name Fields.divide}; (*Build term (p / q) * t*) fun mk_fcoeff ((p, q), t) = @@ -106,7 +106,7 @@ (*Express t as a product of a fraction with other sorted terms*) fun dest_fcoeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_fcoeff (~sign) t - | dest_fcoeff sign (Const (@{const_name Rings.divide}, _) $ t $ u) = + | dest_fcoeff sign (Const (@{const_name Fields.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 Rings.divide} - val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} Term.dummyT + val mk_bal = HOLogic.mk_binop @{const_name Fields.divide} + val dest_bal = HOLogic.dest_bin @{const_name Fields.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 Rings.divide} - val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} Term.dummyT + val mk_bal = HOLogic.mk_binop @{const_name Fields.divide} + val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if} ); @@ -639,13 +639,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 Rings.divide},_)$_$_, _) => + (Const(@{const_name Fields.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 (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz) end - | (_, Const (@{const_name Rings.divide},_)$_$_) => + | (_, Const (@{const_name Fields.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 @@ -655,49 +655,49 @@ end handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE - fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b + fun is_number (Const(@{const_name Fields.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 Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => + Const(@{const_name Orderings.less},_)$(Const(@{const_name Fields.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 Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => + | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Fields.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(@{const_name HOL.eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => + | Const(@{const_name HOL.eq},_)$(Const(@{const_name Fields.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 Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => + | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Fields.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 Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => + | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Fields.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(@{const_name HOL.eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => + | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Fields.divide},_)$_$_) => let val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop val _ = map is_number [a,b,c] diff -r 4588597ba37e -r 5bce8ff0d9ae src/HOL/Tools/semiring_normalizer.ML --- a/src/HOL/Tools/semiring_normalizer.ML Mon Aug 08 08:55:49 2011 -0700 +++ b/src/HOL/Tools/semiring_normalizer.ML Mon Aug 08 09:52:09 2011 -0700 @@ -185,14 +185,14 @@ let fun numeral_is_const ct = case term_of ct of - Const (@{const_name Rings.divide},_) $ a $ b => + Const (@{const_name Fields.divide},_) $ a $ b => can HOLogic.dest_number a andalso can HOLogic.dest_number b - | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t + | Const (@{const_name Fields.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 Rings.divide},_) $ a $ b=> + Const (@{const_name Fields.divide},_) $ a $ b=> Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) - | Const (@{const_name Rings.inverse},_)$t => + | Const (@{const_name Fields.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") diff -r 4588597ba37e -r 5bce8ff0d9ae src/HOL/ex/SVC_Oracle.thy --- a/src/HOL/ex/SVC_Oracle.thy Mon Aug 08 08:55:49 2011 -0700 +++ b/src/HOL/ex/SVC_Oracle.thy Mon Aug 08 09:52:09 2011 -0700 @@ -64,7 +64,7 @@ (*abstraction of a real/rational expression*) fun rat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y) | rat ((c as Const(@{const_name Groups.minus}, _)) $ 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 Fields.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y) | rat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (rat x) $ (rat y) | rat ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (rat x) | rat t = lit t diff -r 4588597ba37e -r 5bce8ff0d9ae src/HOL/ex/svc_funcs.ML --- a/src/HOL/ex/svc_funcs.ML Mon Aug 08 08:55:49 2011 -0700 +++ b/src/HOL/ex/svc_funcs.ML Mon Aug 08 09:52:09 2011 -0700 @@ -173,7 +173,7 @@ | tm (Const(@{const_name Groups.times}, T) $ x $ y) = if is_numeric_op T then Interp("*", [tm x, tm y]) else fail t - | tm (Const(@{const_name Rings.inverse}, T) $ x) = + | tm (Const(@{const_name Fields.inverse}, T) $ x) = if domain_type T = HOLogic.realT then Rat(1, litExp x) else fail t