--- 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
--- 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"
--- 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
--- 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"
--- 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>"
--- 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"
--- 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>
--- 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
--- 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)