# HG changeset patch
# User haftmann
# Date 1476809333 -7200
# Node ID fb5c74a587968612dcc23c71e74d34a1c917c7a2
# Parent  42f28160bad92d9e1ff94a4433543269c4e89db0
suitable logical type class for abs, sgn

diff -r 42f28160bad9 -r fb5c74a58796 NEWS
--- a/NEWS	Tue Oct 18 17:29:28 2016 +0200
+++ b/NEWS	Tue Oct 18 18:48:53 2016 +0200
@@ -281,6 +281,10 @@
     mod_1 ~> mod_by_Suc_0
 INCOMPATIBILITY.
 
+* New type class "idom_abs_sgn" specifies algebraic properties
+of sign and absolute value functions.  Type class "sgn_if" has
+disappeared.  Slight INCOMPATIBILITY.
+
 * Dedicated syntax LENGTH('a) for length of types.
 
 * New proof method "argo" using the built-in Argo solver based on SMT
diff -r 42f28160bad9 -r fb5c74a58796 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Oct 18 17:29:28 2016 +0200
+++ b/src/HOL/Complex.thy	Tue Oct 18 18:48:53 2016 +0200
@@ -381,6 +381,23 @@
   by (simp add: complex_sgn_def divide_inverse)
 
 
+subsection \<open>Absolute value\<close>
+
+instantiation complex :: field_abs_sgn
+begin
+
+definition abs_complex :: "complex \<Rightarrow> complex"
+  where "abs_complex = of_real \<circ> norm"
+
+instance
+  apply standard
+         apply (auto simp add: abs_complex_def complex_sgn_def norm_mult)
+  apply (auto simp add: scaleR_conv_of_real field_simps)
+  done
+
+end
+
+
 subsection \<open>Completeness of the Complexes\<close>
 
 lemma bounded_linear_Re: "bounded_linear Re"
diff -r 42f28160bad9 -r fb5c74a58796 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Tue Oct 18 17:29:28 2016 +0200
+++ b/src/HOL/Enum.thy	Tue Oct 18 18:48:53 2016 +0200
@@ -580,7 +580,7 @@
 instantiation finite_1 :: 
   "{linordered_ring_strict, linordered_comm_semiring_strict, ordered_comm_ring,
     ordered_cancel_comm_monoid_diff, comm_monoid_mult, ordered_ring_abs,
-    one, modulo, sgn_if, inverse}"
+    one, modulo, sgn, inverse}"
 begin
 definition [simp]: "Groups.zero = a\<^sub>1"
 definition [simp]: "Groups.one = a\<^sub>1"
@@ -683,7 +683,7 @@
 
 instance finite_2 :: complete_linorder ..
 
-instantiation finite_2 :: "{field, abs_if, ring_div, sgn_if, semiring_div}" begin
+instantiation finite_2 :: "{field, ring_div, idom_abs_sgn}" begin
 definition [simp]: "0 = a\<^sub>1"
 definition [simp]: "1 = a\<^sub>2"
 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)"
@@ -806,7 +806,7 @@
 
 instance finite_3 :: complete_linorder ..
 
-instantiation finite_3 :: "{field, abs_if, ring_div, semiring_div, sgn_if}" begin
+instantiation finite_3 :: "{field, ring_div, idom_abs_sgn}" begin
 definition [simp]: "0 = a\<^sub>1"
 definition [simp]: "1 = a\<^sub>2"
 definition
@@ -819,9 +819,9 @@
 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)"
 definition "inverse = (\<lambda>x :: finite_3. x)" 
 definition "x div y = x * inverse (y :: finite_3)"
-definition "abs = (\<lambda>x :: finite_3. x)"
+definition "abs = (\<lambda>x. case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
 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)"
-definition "sgn = (\<lambda>x. case x of a\<^sub>1 \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
+definition "sgn = (\<lambda>x :: finite_3. x)"
 instance
 by intro_classes
   (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
diff -r 42f28160bad9 -r fb5c74a58796 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Tue Oct 18 17:29:28 2016 +0200
+++ b/src/HOL/Fields.thy	Tue Oct 18 18:48:53 2016 +0200
@@ -513,6 +513,48 @@
 
 subsection \<open>Ordered fields\<close>
 
+class field_abs_sgn = field + idom_abs_sgn
+begin
+
+lemma sgn_inverse [simp]:
+  "sgn (inverse a) = inverse (sgn a)"
+proof (cases "a = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  then have "a * inverse a = 1"
+    by simp
+  then have "sgn (a * inverse a) = sgn 1"
+    by simp
+  then have "sgn a * sgn (inverse a) = 1"
+    by (simp add: sgn_mult)
+  then have "inverse (sgn a) * (sgn a * sgn (inverse a)) = inverse (sgn a) * 1"
+    by simp
+  then have "(inverse (sgn a) * sgn a) * sgn (inverse a) = inverse (sgn a)"
+    by (simp add: ac_simps)
+  with False show ?thesis
+    by (simp add: sgn_eq_0_iff)
+qed
+
+lemma abs_inverse [simp]:
+  "\<bar>inverse a\<bar> = inverse \<bar>a\<bar>"
+proof -
+  from sgn_mult_abs [of "inverse a"] sgn_mult_abs [of a]
+  have "inverse (sgn a) * \<bar>inverse a\<bar> = inverse (sgn a * \<bar>a\<bar>)"
+    by simp
+  then show ?thesis by (auto simp add: sgn_eq_0_iff)
+qed
+    
+lemma sgn_divide [simp]:
+  "sgn (a / b) = sgn a / sgn b"
+  unfolding divide_inverse sgn_mult by simp
+
+lemma abs_divide [simp]:
+  "\<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
+  unfolding divide_inverse abs_mult by simp
+  
+end
+
 class linordered_field = field + linordered_idom
 begin
 
@@ -932,16 +974,15 @@
   show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
 qed
 
+subclass field_abs_sgn ..
+
 lemma nonzero_abs_inverse:
-     "a \<noteq> 0 ==> \<bar>inverse a\<bar> = inverse \<bar>a\<bar>"
-apply (auto simp add: neq_iff abs_if nonzero_inverse_minus_eq
-                      negative_imp_inverse_negative)
-apply (blast intro: positive_imp_inverse_positive elim: less_asym)
-done
+  "a \<noteq> 0 ==> \<bar>inverse a\<bar> = inverse \<bar>a\<bar>"
+  by (rule abs_inverse)
 
 lemma nonzero_abs_divide:
-     "b \<noteq> 0 ==> \<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
-  by (simp add: divide_inverse abs_mult nonzero_abs_inverse)
+  "b \<noteq> 0 ==> \<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
+  by (rule abs_divide)
 
 lemma field_le_epsilon:
   assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
@@ -1147,19 +1188,6 @@
   "(b/a = 1) = ((a \<noteq> 0 & a = b))"
 by (auto simp add: divide_eq_eq)
 
-lemma abs_inverse [simp]:
-     "\<bar>inverse a\<bar> =
-      inverse \<bar>a\<bar>"
-apply (cases "a=0", simp)
-apply (simp add: nonzero_abs_inverse)
-done
-
-lemma abs_divide [simp]:
-     "\<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
-apply (cases "b=0", simp)
-apply (simp add: nonzero_abs_divide)
-done
-
 lemma abs_div_pos: "0 < y ==>
     \<bar>x\<bar> / y = \<bar>x / y\<bar>"
   apply (subst abs_divide)
@@ -1174,7 +1202,7 @@
 
 lemma inverse_sgn:
   "sgn (inverse a) = inverse (sgn a)"
-  by (simp add: sgn_if)
+  by (fact sgn_inverse)
 
 lemma field_le_mult_one_interval:
   assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
diff -r 42f28160bad9 -r fb5c74a58796 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Tue Oct 18 17:29:28 2016 +0200
+++ b/src/HOL/Groups.thy	Tue Oct 18 18:48:53 2016 +0200
@@ -1148,18 +1148,6 @@
 class sgn =
   fixes sgn :: "'a \<Rightarrow> 'a"
 
-class abs_if = minus + uminus + ord + zero + abs +
-  assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
-
-class sgn_if = minus + uminus + zero + one + ord + sgn +
-  assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
-begin
-
-lemma sgn0 [simp]: "sgn 0 = 0"
-  by (simp add:sgn_if)
-
-end
-
 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
     and abs_ge_self: "a \<le> \<bar>a\<bar>"
diff -r 42f28160bad9 -r fb5c74a58796 src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Tue Oct 18 17:29:28 2016 +0200
+++ b/src/HOL/Library/Fraction_Field.thy	Tue Oct 18 18:48:53 2016 +0200
@@ -70,7 +70,7 @@
     and "\<And>a c. Fract 0 a = Fract 0 c"
 by(transfer; simp)+
 
-instantiation fract :: (idom) "{comm_ring_1,power}"
+instantiation fract :: (idom) comm_ring_1
 begin
 
 lift_definition zero_fract :: "'a fract" is "(0, 1)" by simp
@@ -353,31 +353,20 @@
 
 end
 
-instantiation fract :: (linordered_idom) "{distrib_lattice,abs_if,sgn_if}"
+instantiation fract :: (linordered_idom) linordered_field
 begin
 
-definition abs_fract_def2: "\<bar>q\<bar> = (if q < 0 then -q else (q::'a fract))"
+definition abs_fract_def2:
+  "\<bar>q\<bar> = (if q < 0 then -q else (q::'a fract))"
 
 definition sgn_fract_def:
   "sgn (q::'a fract) = (if q = 0 then 0 else if 0 < q then 1 else - 1)"
 
 theorem abs_fract [simp]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
-unfolding abs_fract_def2 not_le[symmetric]
-by transfer(auto simp add: zero_less_mult_iff le_less)
-
-definition inf_fract_def:
-  "(inf :: 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = min"
+  unfolding abs_fract_def2 not_le [symmetric]
+  by transfer (auto simp add: zero_less_mult_iff le_less)
 
-definition sup_fract_def:
-  "(sup :: 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = max"
-
-instance
-by intro_classes (simp_all add: abs_fract_def2 sgn_fract_def inf_fract_def sup_fract_def max_min_distrib2)
-
-end
-
-instance fract :: (linordered_idom) linordered_field
-proof
+instance proof
   fix q r s :: "'a fract"
   assume "q \<le> r"
   then show "s + q \<le> s + r"
@@ -420,7 +409,23 @@
         by (simp add: ac_simps)
     qed
   qed
-qed
+qed (fact sgn_fract_def abs_fract_def2)+
+
+end
+
+instantiation fract :: (linordered_idom) distrib_lattice
+begin
+
+definition inf_fract_def:
+  "(inf :: 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = min"
+
+definition sup_fract_def:
+  "(sup :: 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = max"
+
+instance
+  by standard (simp_all add: inf_fract_def sup_fract_def max_min_distrib2)
+  
+end
 
 lemma fract_induct_pos [case_names Fract]:
   fixes P :: "'a::linordered_idom fract \<Rightarrow> bool"
diff -r 42f28160bad9 -r fb5c74a58796 src/HOL/Nonstandard_Analysis/StarDef.thy
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Tue Oct 18 17:29:28 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Tue Oct 18 18:48:53 2016 +0200
@@ -898,19 +898,15 @@
 instance star :: (abs_if) abs_if
   by (intro_classes; transfer) (fact abs_if)
 
-instance star :: (sgn_if) sgn_if
-  by (intro_classes; transfer) (fact sgn_if)
-
 instance star :: (linordered_ring_strict) linordered_ring_strict ..
 instance star :: (ordered_comm_ring) ordered_comm_ring ..
 
 instance star :: (linordered_semidom) linordered_semidom
-  apply intro_classes
-  apply(transfer, fact zero_less_one)
-  apply(transfer, fact le_add_diff_inverse2)
-  done
+  by (intro_classes; transfer) (fact zero_less_one le_add_diff_inverse2)+
 
-instance star :: (linordered_idom) linordered_idom ..
+instance star :: (linordered_idom) linordered_idom
+  by (intro_classes; transfer) (fact sgn_if)
+
 instance star :: (linordered_field) linordered_field ..
 
 subsection \<open>Power\<close>
diff -r 42f28160bad9 -r fb5c74a58796 src/HOL/Quotient_Examples/Quotient_Rat.thy
--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Tue Oct 18 17:29:28 2016 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Tue Oct 18 18:48:53 2016 +0200
@@ -28,7 +28,7 @@
 quotient_type rat = "int \<times> int" / partial: ratrel
  using ratrel_equivp .
 
-instantiation rat :: "{zero, one, plus, uminus, minus, times, ord, abs_if, sgn_if}"
+instantiation rat :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
 begin
 
 quotient_definition
@@ -100,8 +100,7 @@
 definition
   sgn_rat_def: "sgn (i::rat) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
 
-instance by intro_classes
-  (auto simp add: rabs_rat_def sgn_rat_def)
+instance ..
 
 end
 
diff -r 42f28160bad9 -r fb5c74a58796 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Tue Oct 18 17:29:28 2016 +0200
+++ b/src/HOL/Rings.thy	Tue Oct 18 18:48:53 2016 +0200
@@ -532,6 +532,100 @@
 
 end
 
+class idom_abs_sgn = idom + abs + sgn +
+  assumes sgn_mult_abs: "sgn a * \<bar>a\<bar> = a"
+    and sgn_sgn [simp]: "sgn (sgn a) = sgn a"
+    and abs_abs [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
+    and abs_0 [simp]: "\<bar>0\<bar> = 0"
+    and sgn_0 [simp]: "sgn 0 = 0"
+    and sgn_1 [simp]: "sgn 1 = 1"
+    and sgn_minus_1: "sgn (- 1) = - 1"
+    and sgn_mult: "sgn (a * b) = sgn a * sgn b"
+begin
+
+lemma sgn_eq_0_iff:
+  "sgn a = 0 \<longleftrightarrow> a = 0"
+proof -
+  { assume "sgn a = 0"
+    then have "sgn a * \<bar>a\<bar> = 0"
+      by simp
+    then have "a = 0"
+      by (simp add: sgn_mult_abs)
+  } then show ?thesis
+    by auto
+qed
+
+lemma abs_eq_0_iff:
+  "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
+proof -
+  { assume "\<bar>a\<bar> = 0"
+    then have "sgn a * \<bar>a\<bar> = 0"
+      by simp
+    then have "a = 0"
+      by (simp add: sgn_mult_abs)
+  } then show ?thesis
+    by auto
+qed
+
+lemma abs_mult_sgn:
+  "\<bar>a\<bar> * sgn a = a"
+  using sgn_mult_abs [of a] by (simp add: ac_simps)
+
+lemma abs_1 [simp]:
+  "\<bar>1\<bar> = 1"
+  using sgn_mult_abs [of 1] by simp
+
+lemma sgn_abs [simp]:
+  "\<bar>sgn a\<bar> = of_bool (a \<noteq> 0)"
+  using sgn_mult_abs [of "sgn a"] mult_cancel_left [of "sgn a" "\<bar>sgn a\<bar>" 1]
+  by (auto simp add: sgn_eq_0_iff)
+
+lemma abs_sgn [simp]:
+  "sgn \<bar>a\<bar> = of_bool (a \<noteq> 0)"
+  using sgn_mult_abs [of "\<bar>a\<bar>"] mult_cancel_right [of "sgn \<bar>a\<bar>" "\<bar>a\<bar>" 1]
+  by (auto simp add: abs_eq_0_iff)
+
+lemma abs_mult:
+  "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
+proof (cases "a = 0 \<or> b = 0")
+  case True
+  then show ?thesis
+    by auto
+next
+  case False
+  then have *: "sgn (a * b) \<noteq> 0"
+    by (simp add: sgn_eq_0_iff)
+  from abs_mult_sgn [of "a * b"] abs_mult_sgn [of a] abs_mult_sgn [of b]
+  have "\<bar>a * b\<bar> * sgn (a * b) = \<bar>a\<bar> * sgn a * \<bar>b\<bar> * sgn b"
+    by (simp add: ac_simps)
+  then have "\<bar>a * b\<bar> * sgn (a * b) = \<bar>a\<bar> * \<bar>b\<bar> * sgn (a * b)"
+    by (simp add: sgn_mult ac_simps)
+  with * show ?thesis
+    by simp
+qed
+
+lemma sgn_minus [simp]:
+  "sgn (- a) = - sgn a"
+proof -
+  from sgn_minus_1 have "sgn (- 1 * a) = - 1 * sgn a"
+    by (simp only: sgn_mult)
+  then show ?thesis
+    by simp
+qed
+
+lemma abs_minus [simp]:
+  "\<bar>- a\<bar> = \<bar>a\<bar>"
+proof -
+  have [simp]: "\<bar>- 1\<bar> = 1"
+    using sgn_mult_abs [of "- 1"] by simp
+  then have "\<bar>- 1 * a\<bar> = 1 * \<bar>a\<bar>"
+    by (simp only: abs_mult)
+  then show ?thesis
+    by simp
+qed
+
+end
+
 text \<open>
   The theory of partially ordered rings is taken from the books:
     \<^item> \<^emph>\<open>Lattice Theory\<close> by Garret Birkhoff, American Mathematical Society, 1979
@@ -1599,6 +1693,9 @@
 
 end
 
+class abs_if = minus + uminus + ord + zero + abs +
+  assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
+
 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
 begin
 
@@ -1842,7 +1939,8 @@
 end
 
 class linordered_idom =
-  comm_ring_1 + linordered_comm_semiring_strict + ordered_ab_group_add + abs_if + sgn_if
+  comm_ring_1 + linordered_comm_semiring_strict + ordered_ab_group_add + abs_if + sgn +
+  assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
 begin
 
 subclass linordered_semiring_1_strict ..
@@ -1857,6 +1955,10 @@
   show "b \<le> a \<Longrightarrow> a - b + b = a" for a b by simp
 qed
 
+subclass idom_abs_sgn
+  by standard
+    (auto simp add: sgn_if abs_if zero_less_mult_iff)
+
 lemma linorder_neqE_linordered_idom:
   assumes "x \<noteq> y"
   obtains "x < y" | "y < x"
@@ -1888,11 +1990,8 @@
 lemma mult_less_cancel_left2: "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
   using mult_less_cancel_left [of c a 1] by simp
 
-lemma sgn_sgn [simp]: "sgn (sgn a) = sgn a"
-  unfolding sgn_if by simp
-
 lemma sgn_0_0: "sgn a = 0 \<longleftrightarrow> a = 0"
-  unfolding sgn_if by simp
+  by (fact sgn_eq_0_iff)
 
 lemma sgn_1_pos: "sgn a = 1 \<longleftrightarrow> a > 0"
   unfolding sgn_if by simp
@@ -1906,9 +2005,6 @@
 lemma sgn_neg [simp]: "a < 0 \<Longrightarrow> sgn a = - 1"
   by (simp only: sgn_1_neg)
 
-lemma sgn_mult: "sgn (a * b) = sgn a * sgn b"
-  by (auto simp add: sgn_if zero_less_mult_iff)
-
 lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
   unfolding sgn_if abs_if by auto
 
@@ -1920,7 +2016,7 @@
 
 lemma abs_sgn_eq_1 [simp]:
   "a \<noteq> 0 \<Longrightarrow> \<bar>sgn a\<bar> = 1"
-  by (simp add: abs_if)
+  by simp
 
 lemma abs_sgn_eq: "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
   by (simp add: sgn_if)
@@ -2005,10 +2101,10 @@
 begin
 
 lemma mult_sgn_abs: "sgn x * \<bar>x\<bar> = x"
-  unfolding abs_if sgn_if by auto
+  by (fact sgn_mult_abs)
 
-lemma abs_one [simp]: "\<bar>1\<bar> = 1"
-  by (simp add: abs_if)
+lemma abs_one: "\<bar>1\<bar> = 1"
+  by (fact abs_1)
 
 end
 
@@ -2022,9 +2118,6 @@
 subclass ordered_ring_abs
   by standard (auto simp: abs_if not_less mult_less_0_iff)
 
-lemma abs_mult: "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
-  by (rule abs_eq_mult) auto
-
 lemma abs_mult_self [simp]: "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
   by (simp add: abs_if)