--- 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))
--- 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));
--- 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 \<Rightarrow> 'a"
+ and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70)
+
+class division_ring = ring_1 + inverse +
+ assumes left_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
+ assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> 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 \<noteq> 0" and b: "b \<noteq> 0"
+ show "a * b \<noteq> 0"
+ proof
+ assume ab: "a * b = 0"
+ hence "0 = inverse a * (a * b) * inverse b" by simp
+ also have "\<dots> = (inverse a * a) * (b * inverse b)"
+ by (simp only: mult_assoc)
+ also have "\<dots> = 1" using a b by simp
+ finally show False by simp
+ qed
+qed
+
+lemma nonzero_imp_inverse_nonzero:
+ "a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0"
+proof
+ assume ianz: "inverse a = 0"
+ assume "a \<noteq> 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 \<Longrightarrow> 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 \<noteq> 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 \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"
+by (rule inverse_unique) simp
+
+lemma nonzero_inverse_inverse_eq:
+ "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a"
+by (rule inverse_unique) simp
+
+lemma nonzero_inverse_eq_imp_eq:
+ assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"
+ shows "a = b"
+proof -
+ from `inverse a = inverse b`
+ have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong)
+ with `a \<noteq> 0` and `b \<noteq> 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 \<noteq> 0" and "b \<noteq> 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 \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b"
+by (simp add: algebra_simps)
+
+lemma division_ring_inverse_diff:
+ "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"
+by (simp add: algebra_simps)
+
+lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
+proof
+ assume neq: "b \<noteq> 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 \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
+by (simp add: divide_inverse)
+
+lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> 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 \<noteq> 0 ==> - (a / b) = a / (- b)"
+ by (simp add: divide_inverse nonzero_inverse_minus_eq)
+
+lemma nonzero_minus_divide_divide: "b \<noteq> 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 \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
+proof -
+ assume [simp]: "c \<noteq> 0"
+ have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
+ also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma nonzero_divide_eq_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
+proof -
+ assume [simp]: "c \<noteq> 0"
+ have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
+ also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
+ by (simp add: divide_inverse mult_assoc)
+
+lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> 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 \<longleftrightarrow> 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\<noteq>0"
+ thus ?thesis by (simp add: nonzero_inverse_minus_eq)
+qed
+
+lemma inverse_eq_imp_eq:
+ "inverse a = inverse b \<Longrightarrow> 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 \<longleftrightarrow> 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\<noteq>0"
+ thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
+qed
+
+end
+
+subsection {* Fields *}
+
class field = comm_ring_1 + inverse +
assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> 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
--- 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";
--- 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 \<Rightarrow> real \<Rightarrow> bool"
real_le > Orderings.ord_class.less_eq :: "real \<Rightarrow> real \<Rightarrow> bool"
real_gt > Orderings.ord_class.greater :: "real \<Rightarrow> real \<Rightarrow> bool"
--- 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"}),
--- 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 \<Rightarrow> 'a"
- and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70)
-
-class division_ring = ring_1 + inverse +
- assumes left_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
- assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> 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 \<noteq> 0" and b: "b \<noteq> 0"
- show "a * b \<noteq> 0"
- proof
- assume ab: "a * b = 0"
- hence "0 = inverse a * (a * b) * inverse b" by simp
- also have "\<dots> = (inverse a * a) * (b * inverse b)"
- by (simp only: mult_assoc)
- also have "\<dots> = 1" using a b by simp
- finally show False by simp
- qed
-qed
-
-lemma nonzero_imp_inverse_nonzero:
- "a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0"
-proof
- assume ianz: "inverse a = 0"
- assume "a \<noteq> 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 \<Longrightarrow> 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 \<noteq> 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 \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"
-by (rule inverse_unique) simp
-
-lemma nonzero_inverse_inverse_eq:
- "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a"
-by (rule inverse_unique) simp
-
-lemma nonzero_inverse_eq_imp_eq:
- assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"
- shows "a = b"
-proof -
- from `inverse a = inverse b`
- have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong)
- with `a \<noteq> 0` and `b \<noteq> 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 \<noteq> 0" and "b \<noteq> 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 \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b"
-by (simp add: algebra_simps)
-
-lemma division_ring_inverse_diff:
- "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"
-by (simp add: algebra_simps)
-
-lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
-proof
- assume neq: "b \<noteq> 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 \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
-by (simp add: divide_inverse)
-
-lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> 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 \<noteq> 0 ==> - (a / b) = a / (- b)"
- by (simp add: divide_inverse nonzero_inverse_minus_eq)
-
-lemma nonzero_minus_divide_divide: "b \<noteq> 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 \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
-proof -
- assume [simp]: "c \<noteq> 0"
- have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
- also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)
- finally show ?thesis .
-qed
-
-lemma nonzero_divide_eq_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
-proof -
- assume [simp]: "c \<noteq> 0"
- have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
- also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc)
- finally show ?thesis .
-qed
-
-lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
- by (simp add: divide_inverse mult_assoc)
-
-lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> 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 \<longleftrightarrow> 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\<noteq>0"
- thus ?thesis by (simp add: nonzero_inverse_minus_eq)
-qed
-
-lemma inverse_eq_imp_eq:
- "inverse a = inverse b \<Longrightarrow> 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 \<longleftrightarrow> 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\<noteq>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}
--- 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)
--- 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]
--- 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")
--- 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
--- 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