suitable logical type class for abs, sgn
authorhaftmann
Tue Oct 18 18:48:53 2016 +0200 (2016-10-18)
changeset 64290fb5c74a58796
parent 64289 42f28160bad9
child 64292 bad166cb5121
suitable logical type class for abs, sgn
NEWS
src/HOL/Complex.thy
src/HOL/Enum.thy
src/HOL/Fields.thy
src/HOL/Groups.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/Nonstandard_Analysis/StarDef.thy
src/HOL/Quotient_Examples/Quotient_Rat.thy
src/HOL/Rings.thy
     1.1 --- a/NEWS	Tue Oct 18 17:29:28 2016 +0200
     1.2 +++ b/NEWS	Tue Oct 18 18:48:53 2016 +0200
     1.3 @@ -281,6 +281,10 @@
     1.4      mod_1 ~> mod_by_Suc_0
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* New type class "idom_abs_sgn" specifies algebraic properties
     1.8 +of sign and absolute value functions.  Type class "sgn_if" has
     1.9 +disappeared.  Slight INCOMPATIBILITY.
    1.10 +
    1.11  * Dedicated syntax LENGTH('a) for length of types.
    1.12  
    1.13  * New proof method "argo" using the built-in Argo solver based on SMT
     2.1 --- a/src/HOL/Complex.thy	Tue Oct 18 17:29:28 2016 +0200
     2.2 +++ b/src/HOL/Complex.thy	Tue Oct 18 18:48:53 2016 +0200
     2.3 @@ -381,6 +381,23 @@
     2.4    by (simp add: complex_sgn_def divide_inverse)
     2.5  
     2.6  
     2.7 +subsection \<open>Absolute value\<close>
     2.8 +
     2.9 +instantiation complex :: field_abs_sgn
    2.10 +begin
    2.11 +
    2.12 +definition abs_complex :: "complex \<Rightarrow> complex"
    2.13 +  where "abs_complex = of_real \<circ> norm"
    2.14 +
    2.15 +instance
    2.16 +  apply standard
    2.17 +         apply (auto simp add: abs_complex_def complex_sgn_def norm_mult)
    2.18 +  apply (auto simp add: scaleR_conv_of_real field_simps)
    2.19 +  done
    2.20 +
    2.21 +end
    2.22 +
    2.23 +
    2.24  subsection \<open>Completeness of the Complexes\<close>
    2.25  
    2.26  lemma bounded_linear_Re: "bounded_linear Re"
     3.1 --- a/src/HOL/Enum.thy	Tue Oct 18 17:29:28 2016 +0200
     3.2 +++ b/src/HOL/Enum.thy	Tue Oct 18 18:48:53 2016 +0200
     3.3 @@ -580,7 +580,7 @@
     3.4  instantiation finite_1 :: 
     3.5    "{linordered_ring_strict, linordered_comm_semiring_strict, ordered_comm_ring,
     3.6      ordered_cancel_comm_monoid_diff, comm_monoid_mult, ordered_ring_abs,
     3.7 -    one, modulo, sgn_if, inverse}"
     3.8 +    one, modulo, sgn, inverse}"
     3.9  begin
    3.10  definition [simp]: "Groups.zero = a\<^sub>1"
    3.11  definition [simp]: "Groups.one = a\<^sub>1"
    3.12 @@ -683,7 +683,7 @@
    3.13  
    3.14  instance finite_2 :: complete_linorder ..
    3.15  
    3.16 -instantiation finite_2 :: "{field, abs_if, ring_div, sgn_if, semiring_div}" begin
    3.17 +instantiation finite_2 :: "{field, ring_div, idom_abs_sgn}" begin
    3.18  definition [simp]: "0 = a\<^sub>1"
    3.19  definition [simp]: "1 = a\<^sub>2"
    3.20  definition "x + y = (case (x, y) of (a\<^sub>1, a\<^sub>1) \<Rightarrow> a\<^sub>1 | (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
    3.21 @@ -806,7 +806,7 @@
    3.22  
    3.23  instance finite_3 :: complete_linorder ..
    3.24  
    3.25 -instantiation finite_3 :: "{field, abs_if, ring_div, semiring_div, sgn_if}" begin
    3.26 +instantiation finite_3 :: "{field, ring_div, idom_abs_sgn}" begin
    3.27  definition [simp]: "0 = a\<^sub>1"
    3.28  definition [simp]: "1 = a\<^sub>2"
    3.29  definition
    3.30 @@ -819,9 +819,9 @@
    3.31  definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>3) \<Rightarrow> a\<^sub>2 | (a\<^sub>2, a\<^sub>3) \<Rightarrow> a\<^sub>3 | (a\<^sub>3, a\<^sub>2) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
    3.32  definition "inverse = (\<lambda>x :: finite_3. x)" 
    3.33  definition "x div y = x * inverse (y :: finite_3)"
    3.34 -definition "abs = (\<lambda>x :: finite_3. x)"
    3.35 +definition "abs = (\<lambda>x. case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
    3.36  definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>1) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
    3.37 -definition "sgn = (\<lambda>x. case x of a\<^sub>1 \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
    3.38 +definition "sgn = (\<lambda>x :: finite_3. x)"
    3.39  instance
    3.40  by intro_classes
    3.41    (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
     4.1 --- a/src/HOL/Fields.thy	Tue Oct 18 17:29:28 2016 +0200
     4.2 +++ b/src/HOL/Fields.thy	Tue Oct 18 18:48:53 2016 +0200
     4.3 @@ -513,6 +513,48 @@
     4.4  
     4.5  subsection \<open>Ordered fields\<close>
     4.6  
     4.7 +class field_abs_sgn = field + idom_abs_sgn
     4.8 +begin
     4.9 +
    4.10 +lemma sgn_inverse [simp]:
    4.11 +  "sgn (inverse a) = inverse (sgn a)"
    4.12 +proof (cases "a = 0")
    4.13 +  case True then show ?thesis by simp
    4.14 +next
    4.15 +  case False
    4.16 +  then have "a * inverse a = 1"
    4.17 +    by simp
    4.18 +  then have "sgn (a * inverse a) = sgn 1"
    4.19 +    by simp
    4.20 +  then have "sgn a * sgn (inverse a) = 1"
    4.21 +    by (simp add: sgn_mult)
    4.22 +  then have "inverse (sgn a) * (sgn a * sgn (inverse a)) = inverse (sgn a) * 1"
    4.23 +    by simp
    4.24 +  then have "(inverse (sgn a) * sgn a) * sgn (inverse a) = inverse (sgn a)"
    4.25 +    by (simp add: ac_simps)
    4.26 +  with False show ?thesis
    4.27 +    by (simp add: sgn_eq_0_iff)
    4.28 +qed
    4.29 +
    4.30 +lemma abs_inverse [simp]:
    4.31 +  "\<bar>inverse a\<bar> = inverse \<bar>a\<bar>"
    4.32 +proof -
    4.33 +  from sgn_mult_abs [of "inverse a"] sgn_mult_abs [of a]
    4.34 +  have "inverse (sgn a) * \<bar>inverse a\<bar> = inverse (sgn a * \<bar>a\<bar>)"
    4.35 +    by simp
    4.36 +  then show ?thesis by (auto simp add: sgn_eq_0_iff)
    4.37 +qed
    4.38 +    
    4.39 +lemma sgn_divide [simp]:
    4.40 +  "sgn (a / b) = sgn a / sgn b"
    4.41 +  unfolding divide_inverse sgn_mult by simp
    4.42 +
    4.43 +lemma abs_divide [simp]:
    4.44 +  "\<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
    4.45 +  unfolding divide_inverse abs_mult by simp
    4.46 +  
    4.47 +end
    4.48 +
    4.49  class linordered_field = field + linordered_idom
    4.50  begin
    4.51  
    4.52 @@ -932,16 +974,15 @@
    4.53    show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
    4.54  qed
    4.55  
    4.56 +subclass field_abs_sgn ..
    4.57 +
    4.58  lemma nonzero_abs_inverse:
    4.59 -     "a \<noteq> 0 ==> \<bar>inverse a\<bar> = inverse \<bar>a\<bar>"
    4.60 -apply (auto simp add: neq_iff abs_if nonzero_inverse_minus_eq
    4.61 -                      negative_imp_inverse_negative)
    4.62 -apply (blast intro: positive_imp_inverse_positive elim: less_asym)
    4.63 -done
    4.64 +  "a \<noteq> 0 ==> \<bar>inverse a\<bar> = inverse \<bar>a\<bar>"
    4.65 +  by (rule abs_inverse)
    4.66  
    4.67  lemma nonzero_abs_divide:
    4.68 -     "b \<noteq> 0 ==> \<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
    4.69 -  by (simp add: divide_inverse abs_mult nonzero_abs_inverse)
    4.70 +  "b \<noteq> 0 ==> \<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
    4.71 +  by (rule abs_divide)
    4.72  
    4.73  lemma field_le_epsilon:
    4.74    assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
    4.75 @@ -1147,19 +1188,6 @@
    4.76    "(b/a = 1) = ((a \<noteq> 0 & a = b))"
    4.77  by (auto simp add: divide_eq_eq)
    4.78  
    4.79 -lemma abs_inverse [simp]:
    4.80 -     "\<bar>inverse a\<bar> =
    4.81 -      inverse \<bar>a\<bar>"
    4.82 -apply (cases "a=0", simp)
    4.83 -apply (simp add: nonzero_abs_inverse)
    4.84 -done
    4.85 -
    4.86 -lemma abs_divide [simp]:
    4.87 -     "\<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
    4.88 -apply (cases "b=0", simp)
    4.89 -apply (simp add: nonzero_abs_divide)
    4.90 -done
    4.91 -
    4.92  lemma abs_div_pos: "0 < y ==>
    4.93      \<bar>x\<bar> / y = \<bar>x / y\<bar>"
    4.94    apply (subst abs_divide)
    4.95 @@ -1174,7 +1202,7 @@
    4.96  
    4.97  lemma inverse_sgn:
    4.98    "sgn (inverse a) = inverse (sgn a)"
    4.99 -  by (simp add: sgn_if)
   4.100 +  by (fact sgn_inverse)
   4.101  
   4.102  lemma field_le_mult_one_interval:
   4.103    assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
     5.1 --- a/src/HOL/Groups.thy	Tue Oct 18 17:29:28 2016 +0200
     5.2 +++ b/src/HOL/Groups.thy	Tue Oct 18 18:48:53 2016 +0200
     5.3 @@ -1148,18 +1148,6 @@
     5.4  class sgn =
     5.5    fixes sgn :: "'a \<Rightarrow> 'a"
     5.6  
     5.7 -class abs_if = minus + uminus + ord + zero + abs +
     5.8 -  assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
     5.9 -
    5.10 -class sgn_if = minus + uminus + zero + one + ord + sgn +
    5.11 -  assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
    5.12 -begin
    5.13 -
    5.14 -lemma sgn0 [simp]: "sgn 0 = 0"
    5.15 -  by (simp add:sgn_if)
    5.16 -
    5.17 -end
    5.18 -
    5.19  class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
    5.20    assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
    5.21      and abs_ge_self: "a \<le> \<bar>a\<bar>"
     6.1 --- a/src/HOL/Library/Fraction_Field.thy	Tue Oct 18 17:29:28 2016 +0200
     6.2 +++ b/src/HOL/Library/Fraction_Field.thy	Tue Oct 18 18:48:53 2016 +0200
     6.3 @@ -70,7 +70,7 @@
     6.4      and "\<And>a c. Fract 0 a = Fract 0 c"
     6.5  by(transfer; simp)+
     6.6  
     6.7 -instantiation fract :: (idom) "{comm_ring_1,power}"
     6.8 +instantiation fract :: (idom) comm_ring_1
     6.9  begin
    6.10  
    6.11  lift_definition zero_fract :: "'a fract" is "(0, 1)" by simp
    6.12 @@ -353,31 +353,20 @@
    6.13  
    6.14  end
    6.15  
    6.16 -instantiation fract :: (linordered_idom) "{distrib_lattice,abs_if,sgn_if}"
    6.17 +instantiation fract :: (linordered_idom) linordered_field
    6.18  begin
    6.19  
    6.20 -definition abs_fract_def2: "\<bar>q\<bar> = (if q < 0 then -q else (q::'a fract))"
    6.21 +definition abs_fract_def2:
    6.22 +  "\<bar>q\<bar> = (if q < 0 then -q else (q::'a fract))"
    6.23  
    6.24  definition sgn_fract_def:
    6.25    "sgn (q::'a fract) = (if q = 0 then 0 else if 0 < q then 1 else - 1)"
    6.26  
    6.27  theorem abs_fract [simp]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
    6.28 -unfolding abs_fract_def2 not_le[symmetric]
    6.29 -by transfer(auto simp add: zero_less_mult_iff le_less)
    6.30 -
    6.31 -definition inf_fract_def:
    6.32 -  "(inf :: 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = min"
    6.33 +  unfolding abs_fract_def2 not_le [symmetric]
    6.34 +  by transfer (auto simp add: zero_less_mult_iff le_less)
    6.35  
    6.36 -definition sup_fract_def:
    6.37 -  "(sup :: 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = max"
    6.38 -
    6.39 -instance
    6.40 -by intro_classes (simp_all add: abs_fract_def2 sgn_fract_def inf_fract_def sup_fract_def max_min_distrib2)
    6.41 -
    6.42 -end
    6.43 -
    6.44 -instance fract :: (linordered_idom) linordered_field
    6.45 -proof
    6.46 +instance proof
    6.47    fix q r s :: "'a fract"
    6.48    assume "q \<le> r"
    6.49    then show "s + q \<le> s + r"
    6.50 @@ -420,7 +409,23 @@
    6.51          by (simp add: ac_simps)
    6.52      qed
    6.53    qed
    6.54 -qed
    6.55 +qed (fact sgn_fract_def abs_fract_def2)+
    6.56 +
    6.57 +end
    6.58 +
    6.59 +instantiation fract :: (linordered_idom) distrib_lattice
    6.60 +begin
    6.61 +
    6.62 +definition inf_fract_def:
    6.63 +  "(inf :: 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = min"
    6.64 +
    6.65 +definition sup_fract_def:
    6.66 +  "(sup :: 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = max"
    6.67 +
    6.68 +instance
    6.69 +  by standard (simp_all add: inf_fract_def sup_fract_def max_min_distrib2)
    6.70 +  
    6.71 +end
    6.72  
    6.73  lemma fract_induct_pos [case_names Fract]:
    6.74    fixes P :: "'a::linordered_idom fract \<Rightarrow> bool"
     7.1 --- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Tue Oct 18 17:29:28 2016 +0200
     7.2 +++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Tue Oct 18 18:48:53 2016 +0200
     7.3 @@ -898,19 +898,15 @@
     7.4  instance star :: (abs_if) abs_if
     7.5    by (intro_classes; transfer) (fact abs_if)
     7.6  
     7.7 -instance star :: (sgn_if) sgn_if
     7.8 -  by (intro_classes; transfer) (fact sgn_if)
     7.9 -
    7.10  instance star :: (linordered_ring_strict) linordered_ring_strict ..
    7.11  instance star :: (ordered_comm_ring) ordered_comm_ring ..
    7.12  
    7.13  instance star :: (linordered_semidom) linordered_semidom
    7.14 -  apply intro_classes
    7.15 -  apply(transfer, fact zero_less_one)
    7.16 -  apply(transfer, fact le_add_diff_inverse2)
    7.17 -  done
    7.18 +  by (intro_classes; transfer) (fact zero_less_one le_add_diff_inverse2)+
    7.19  
    7.20 -instance star :: (linordered_idom) linordered_idom ..
    7.21 +instance star :: (linordered_idom) linordered_idom
    7.22 +  by (intro_classes; transfer) (fact sgn_if)
    7.23 +
    7.24  instance star :: (linordered_field) linordered_field ..
    7.25  
    7.26  subsection \<open>Power\<close>
     8.1 --- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Tue Oct 18 17:29:28 2016 +0200
     8.2 +++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Tue Oct 18 18:48:53 2016 +0200
     8.3 @@ -28,7 +28,7 @@
     8.4  quotient_type rat = "int \<times> int" / partial: ratrel
     8.5   using ratrel_equivp .
     8.6  
     8.7 -instantiation rat :: "{zero, one, plus, uminus, minus, times, ord, abs_if, sgn_if}"
     8.8 +instantiation rat :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
     8.9  begin
    8.10  
    8.11  quotient_definition
    8.12 @@ -100,8 +100,7 @@
    8.13  definition
    8.14    sgn_rat_def: "sgn (i::rat) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
    8.15  
    8.16 -instance by intro_classes
    8.17 -  (auto simp add: rabs_rat_def sgn_rat_def)
    8.18 +instance ..
    8.19  
    8.20  end
    8.21  
     9.1 --- a/src/HOL/Rings.thy	Tue Oct 18 17:29:28 2016 +0200
     9.2 +++ b/src/HOL/Rings.thy	Tue Oct 18 18:48:53 2016 +0200
     9.3 @@ -532,6 +532,100 @@
     9.4  
     9.5  end
     9.6  
     9.7 +class idom_abs_sgn = idom + abs + sgn +
     9.8 +  assumes sgn_mult_abs: "sgn a * \<bar>a\<bar> = a"
     9.9 +    and sgn_sgn [simp]: "sgn (sgn a) = sgn a"
    9.10 +    and abs_abs [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
    9.11 +    and abs_0 [simp]: "\<bar>0\<bar> = 0"
    9.12 +    and sgn_0 [simp]: "sgn 0 = 0"
    9.13 +    and sgn_1 [simp]: "sgn 1 = 1"
    9.14 +    and sgn_minus_1: "sgn (- 1) = - 1"
    9.15 +    and sgn_mult: "sgn (a * b) = sgn a * sgn b"
    9.16 +begin
    9.17 +
    9.18 +lemma sgn_eq_0_iff:
    9.19 +  "sgn a = 0 \<longleftrightarrow> a = 0"
    9.20 +proof -
    9.21 +  { assume "sgn a = 0"
    9.22 +    then have "sgn a * \<bar>a\<bar> = 0"
    9.23 +      by simp
    9.24 +    then have "a = 0"
    9.25 +      by (simp add: sgn_mult_abs)
    9.26 +  } then show ?thesis
    9.27 +    by auto
    9.28 +qed
    9.29 +
    9.30 +lemma abs_eq_0_iff:
    9.31 +  "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
    9.32 +proof -
    9.33 +  { assume "\<bar>a\<bar> = 0"
    9.34 +    then have "sgn a * \<bar>a\<bar> = 0"
    9.35 +      by simp
    9.36 +    then have "a = 0"
    9.37 +      by (simp add: sgn_mult_abs)
    9.38 +  } then show ?thesis
    9.39 +    by auto
    9.40 +qed
    9.41 +
    9.42 +lemma abs_mult_sgn:
    9.43 +  "\<bar>a\<bar> * sgn a = a"
    9.44 +  using sgn_mult_abs [of a] by (simp add: ac_simps)
    9.45 +
    9.46 +lemma abs_1 [simp]:
    9.47 +  "\<bar>1\<bar> = 1"
    9.48 +  using sgn_mult_abs [of 1] by simp
    9.49 +
    9.50 +lemma sgn_abs [simp]:
    9.51 +  "\<bar>sgn a\<bar> = of_bool (a \<noteq> 0)"
    9.52 +  using sgn_mult_abs [of "sgn a"] mult_cancel_left [of "sgn a" "\<bar>sgn a\<bar>" 1]
    9.53 +  by (auto simp add: sgn_eq_0_iff)
    9.54 +
    9.55 +lemma abs_sgn [simp]:
    9.56 +  "sgn \<bar>a\<bar> = of_bool (a \<noteq> 0)"
    9.57 +  using sgn_mult_abs [of "\<bar>a\<bar>"] mult_cancel_right [of "sgn \<bar>a\<bar>" "\<bar>a\<bar>" 1]
    9.58 +  by (auto simp add: abs_eq_0_iff)
    9.59 +
    9.60 +lemma abs_mult:
    9.61 +  "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
    9.62 +proof (cases "a = 0 \<or> b = 0")
    9.63 +  case True
    9.64 +  then show ?thesis
    9.65 +    by auto
    9.66 +next
    9.67 +  case False
    9.68 +  then have *: "sgn (a * b) \<noteq> 0"
    9.69 +    by (simp add: sgn_eq_0_iff)
    9.70 +  from abs_mult_sgn [of "a * b"] abs_mult_sgn [of a] abs_mult_sgn [of b]
    9.71 +  have "\<bar>a * b\<bar> * sgn (a * b) = \<bar>a\<bar> * sgn a * \<bar>b\<bar> * sgn b"
    9.72 +    by (simp add: ac_simps)
    9.73 +  then have "\<bar>a * b\<bar> * sgn (a * b) = \<bar>a\<bar> * \<bar>b\<bar> * sgn (a * b)"
    9.74 +    by (simp add: sgn_mult ac_simps)
    9.75 +  with * show ?thesis
    9.76 +    by simp
    9.77 +qed
    9.78 +
    9.79 +lemma sgn_minus [simp]:
    9.80 +  "sgn (- a) = - sgn a"
    9.81 +proof -
    9.82 +  from sgn_minus_1 have "sgn (- 1 * a) = - 1 * sgn a"
    9.83 +    by (simp only: sgn_mult)
    9.84 +  then show ?thesis
    9.85 +    by simp
    9.86 +qed
    9.87 +
    9.88 +lemma abs_minus [simp]:
    9.89 +  "\<bar>- a\<bar> = \<bar>a\<bar>"
    9.90 +proof -
    9.91 +  have [simp]: "\<bar>- 1\<bar> = 1"
    9.92 +    using sgn_mult_abs [of "- 1"] by simp
    9.93 +  then have "\<bar>- 1 * a\<bar> = 1 * \<bar>a\<bar>"
    9.94 +    by (simp only: abs_mult)
    9.95 +  then show ?thesis
    9.96 +    by simp
    9.97 +qed
    9.98 +
    9.99 +end
   9.100 +
   9.101  text \<open>
   9.102    The theory of partially ordered rings is taken from the books:
   9.103      \<^item> \<^emph>\<open>Lattice Theory\<close> by Garret Birkhoff, American Mathematical Society, 1979
   9.104 @@ -1599,6 +1693,9 @@
   9.105  
   9.106  end
   9.107  
   9.108 +class abs_if = minus + uminus + ord + zero + abs +
   9.109 +  assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
   9.110 +
   9.111  class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
   9.112  begin
   9.113  
   9.114 @@ -1842,7 +1939,8 @@
   9.115  end
   9.116  
   9.117  class linordered_idom =
   9.118 -  comm_ring_1 + linordered_comm_semiring_strict + ordered_ab_group_add + abs_if + sgn_if
   9.119 +  comm_ring_1 + linordered_comm_semiring_strict + ordered_ab_group_add + abs_if + sgn +
   9.120 +  assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
   9.121  begin
   9.122  
   9.123  subclass linordered_semiring_1_strict ..
   9.124 @@ -1857,6 +1955,10 @@
   9.125    show "b \<le> a \<Longrightarrow> a - b + b = a" for a b by simp
   9.126  qed
   9.127  
   9.128 +subclass idom_abs_sgn
   9.129 +  by standard
   9.130 +    (auto simp add: sgn_if abs_if zero_less_mult_iff)
   9.131 +
   9.132  lemma linorder_neqE_linordered_idom:
   9.133    assumes "x \<noteq> y"
   9.134    obtains "x < y" | "y < x"
   9.135 @@ -1888,11 +1990,8 @@
   9.136  lemma mult_less_cancel_left2: "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
   9.137    using mult_less_cancel_left [of c a 1] by simp
   9.138  
   9.139 -lemma sgn_sgn [simp]: "sgn (sgn a) = sgn a"
   9.140 -  unfolding sgn_if by simp
   9.141 -
   9.142  lemma sgn_0_0: "sgn a = 0 \<longleftrightarrow> a = 0"
   9.143 -  unfolding sgn_if by simp
   9.144 +  by (fact sgn_eq_0_iff)
   9.145  
   9.146  lemma sgn_1_pos: "sgn a = 1 \<longleftrightarrow> a > 0"
   9.147    unfolding sgn_if by simp
   9.148 @@ -1906,9 +2005,6 @@
   9.149  lemma sgn_neg [simp]: "a < 0 \<Longrightarrow> sgn a = - 1"
   9.150    by (simp only: sgn_1_neg)
   9.151  
   9.152 -lemma sgn_mult: "sgn (a * b) = sgn a * sgn b"
   9.153 -  by (auto simp add: sgn_if zero_less_mult_iff)
   9.154 -
   9.155  lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
   9.156    unfolding sgn_if abs_if by auto
   9.157  
   9.158 @@ -1920,7 +2016,7 @@
   9.159  
   9.160  lemma abs_sgn_eq_1 [simp]:
   9.161    "a \<noteq> 0 \<Longrightarrow> \<bar>sgn a\<bar> = 1"
   9.162 -  by (simp add: abs_if)
   9.163 +  by simp
   9.164  
   9.165  lemma abs_sgn_eq: "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
   9.166    by (simp add: sgn_if)
   9.167 @@ -2005,10 +2101,10 @@
   9.168  begin
   9.169  
   9.170  lemma mult_sgn_abs: "sgn x * \<bar>x\<bar> = x"
   9.171 -  unfolding abs_if sgn_if by auto
   9.172 +  by (fact sgn_mult_abs)
   9.173  
   9.174 -lemma abs_one [simp]: "\<bar>1\<bar> = 1"
   9.175 -  by (simp add: abs_if)
   9.176 +lemma abs_one: "\<bar>1\<bar> = 1"
   9.177 +  by (fact abs_1)
   9.178  
   9.179  end
   9.180  
   9.181 @@ -2022,9 +2118,6 @@
   9.182  subclass ordered_ring_abs
   9.183    by standard (auto simp: abs_if not_less mult_less_0_iff)
   9.184  
   9.185 -lemma abs_mult: "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
   9.186 -  by (rule abs_eq_mult) auto
   9.187 -
   9.188  lemma abs_mult_self [simp]: "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
   9.189    by (simp add: abs_if)
   9.190