# HG changeset patch
# User haftmann
# Date 1455742317 -3600
# Node ID 2230b70473767df9bd594215df7ea49c0fe6c92b
# Parent  97f2ed2404314092d21d525f6d75581ad5aa8906
generalized some lemmas;
moved some lemmas in more appropriate places;
deleted potentially dangerous simp rule

diff -r 97f2ed240431 -r 2230b7047376 NEWS
--- a/NEWS	Wed Feb 17 21:51:56 2016 +0100
+++ b/NEWS	Wed Feb 17 21:51:57 2016 +0100
@@ -37,6 +37,11 @@
 
 * Class semiring_Lcd merged into semiring_Gcd.  INCOMPATIBILITY.
 
+* Lemma generalization:
+    realpow_minus_mult ~> power_minus_mult
+    realpow_Suc_le_self ~> power_Suc_le_self
+INCOMPATIBILITY.
+
 
 New in Isabelle2016 (February 2016)
 -----------------------------------
diff -r 97f2ed240431 -r 2230b7047376 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/Algebra/Coset.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -936,18 +936,6 @@
   thus ?thesis by (auto simp add: g)
 qed
 
-lemma the_elem_image_unique: -- {* FIXME move *}
-  assumes "A \<noteq> {}"
-  assumes *: "\<And>y. y \<in> A \<Longrightarrow> f y = f x"
-  shows "the_elem (f ` A) = f x"
-unfolding the_elem_def proof (rule the1_equality)
-  from `A \<noteq> {}` obtain y where "y \<in> A" by auto
-  with * have "f x = f y" by simp
-  with `y \<in> A` have "f x \<in> f ` A" by blast
-  with * show "f ` A = {f x}" by auto
-  then show "\<exists>!x. f ` A = {x}" by auto
-qed
-
 lemma (in group_hom) FactGroup_hom:
      "(\<lambda>X. the_elem (h`X)) \<in> hom (G Mod (kernel G H h)) H"
 apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
diff -r 97f2ed240431 -r 2230b7047376 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/Binomial.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -25,9 +25,19 @@
 lemma fact_Suc_0 [simp]: "fact (Suc 0) = Suc 0"
   by simp
 
-lemma of_nat_fact [simp]: "of_nat (fact n) = fact n"
+lemma of_nat_fact [simp]:
+  "of_nat (fact n) = fact n"
   by (induct n) (auto simp add: algebra_simps of_nat_mult)
  
+lemma of_int_fact [simp]:
+  "of_int (fact n) = fact n"
+proof -
+  have "of_int (of_nat (fact n)) = fact n"
+    unfolding of_int_of_nat_eq by simp
+  then show ?thesis
+    by simp
+qed
+
 lemma fact_reduce: "n > 0 \<Longrightarrow> fact n = of_nat n * fact (n - 1)"
   by (cases n) auto
 
diff -r 97f2ed240431 -r 2230b7047376 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/Fields.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -1152,6 +1152,10 @@
 lemma divide_le_0_abs_iff [simp]: "(a / \<bar>b\<bar> \<le> 0) = (a \<le> 0 | b = 0)"
 by (auto simp: divide_le_0_iff)
 
+lemma inverse_sgn:
+  "sgn (inverse a) = inverse (sgn a)"
+  by (simp add: sgn_if)
+
 lemma field_le_mult_one_interval:
   assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
   shows "x \<le> y"
diff -r 97f2ed240431 -r 2230b7047376 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/GCD.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -2057,9 +2057,6 @@
 
 text \<open>Fact aliasses\<close>
 
-lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat \<bar>x\<bar> dvd nat \<bar>y\<bar>"
-  by (fact dvd_int_unfold_dvd_nat)
-
 lemmas gcd_assoc_nat = gcd.assoc [where ?'a = nat]
 lemmas gcd_assoc_int = gcd.assoc [where ?'a = int]
 lemmas gcd_commute_nat = gcd.commute [where ?'a = nat]
diff -r 97f2ed240431 -r 2230b7047376 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/Groups.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -1382,7 +1382,6 @@
 lemmas ab_left_minus = left_minus \<comment> \<open>FIXME duplicate\<close>
 lemmas diff_diff_eq = diff_diff_add \<comment> \<open>FIXME duplicate\<close>
 
-
 subsection \<open>Tools setup\<close>
 
 lemma add_mono_thms_linordered_semiring:
diff -r 97f2ed240431 -r 2230b7047376 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/Int.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -190,6 +190,21 @@
 apply arith
 done
 
+lemma zabs_less_one_iff [simp]:
+  fixes z :: int
+  shows "\<bar>z\<bar> < 1 \<longleftrightarrow> z = 0" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?Q then show ?P by simp
+next
+  assume ?P
+  with zless_imp_add1_zle [of "\<bar>z\<bar>" 1] have "\<bar>z\<bar> + 1 \<le> 1"
+    by simp
+  then have "\<bar>z\<bar> \<le> 0"
+    by simp
+  then show ?Q
+    by simp
+qed
+
 lemmas int_distrib =
   distrib_right [of z1 z2 w]
   distrib_left [of w z1 z2]
@@ -320,6 +335,45 @@
 lemma of_int_nonneg: "z \<ge> 0 \<Longrightarrow> of_int z \<ge> 0"
   by simp
 
+lemma of_int_abs [simp]:
+  "of_int \<bar>x\<bar> = \<bar>of_int x\<bar>"
+  by (auto simp add: abs_if)
+
+lemma of_int_lessD:
+  assumes "\<bar>of_int n\<bar> < x"
+  shows "n = 0 \<or> x > 1"
+proof (cases "n = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  then have "\<bar>n\<bar> \<noteq> 0" by simp
+  then have "\<bar>n\<bar> > 0" by simp
+  then have "\<bar>n\<bar> \<ge> 1"
+    using zless_imp_add1_zle [of 0 "\<bar>n\<bar>"] by simp
+  then have "\<bar>of_int n\<bar> \<ge> 1"
+    unfolding of_int_1_le_iff [of "\<bar>n\<bar>", symmetric] by simp
+  then have "1 < x" using assms by (rule le_less_trans)
+  then show ?thesis ..
+qed
+
+lemma of_int_leD:
+  assumes "\<bar>of_int n\<bar> \<le> x"
+  shows "n = 0 \<or> 1 \<le> x"
+proof (cases "n = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  then have "\<bar>n\<bar> \<noteq> 0" by simp
+  then have "\<bar>n\<bar> > 0" by simp
+  then have "\<bar>n\<bar> \<ge> 1"
+    using zless_imp_add1_zle [of 0 "\<bar>n\<bar>"] by simp
+  then have "\<bar>of_int n\<bar> \<ge> 1"
+    unfolding of_int_1_le_iff [of "\<bar>n\<bar>", symmetric] by simp
+  then have "1 \<le> x" using assms by (rule order_trans)
+  then show ?thesis ..
+qed
+
+
 end
 
 text \<open>Comparisons involving @{term of_int}.\<close>
@@ -1152,9 +1206,6 @@
 
 subsection\<open>Products and 1, by T. M. Rasmussen\<close>
 
-lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
-by arith
-
 lemma abs_zmult_eq_1:
   assumes mn: "\<bar>m * n\<bar> = 1"
   shows "\<bar>m\<bar> = (1::int)"
diff -r 97f2ed240431 -r 2230b7047376 src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/NthRoot.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -10,17 +10,6 @@
 imports Deriv Binomial
 begin
 
-lemma abs_sgn_eq: "\<bar>sgn x :: real\<bar> = (if x = 0 then 0 else 1)"
-  by (simp add: sgn_real_def)
-
-lemma inverse_sgn: "sgn (inverse a) = inverse (sgn a :: real)"
-  by (simp add: sgn_real_def)
-
-lemma power_eq_iff_eq_base:
-  fixes a b :: "_ :: linordered_semidom"
-  shows "0 < n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a ^ n = b ^ n \<longleftrightarrow> a = b"
-  using power_eq_imp_eq_base[of a n b] by auto
-
 subsection \<open>Existence of Nth Root\<close>
 
 text \<open>Existence follows from the Intermediate Value Theorem\<close>
diff -r 97f2ed240431 -r 2230b7047376 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/Power.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -9,19 +9,6 @@
 imports Num Equiv_Relations
 begin
 
-context linordered_ring (* TODO: move *)
-begin
-
-lemma sum_squares_ge_zero:
-  "0 \<le> x * x + y * y"
-  by (intro add_nonneg_nonneg zero_le_square)
-
-lemma not_sum_squares_lt_zero:
-  "\<not> x * x + y * y < 0"
-  by (simp add: not_less sum_squares_ge_zero)
-
-end
-
 subsection \<open>Powers for Arbitrary Monoids\<close>
 
 class power = one + times
@@ -123,6 +110,10 @@
   finally show ?case .
 qed simp
 
+lemma power_minus_mult:
+  "0 < n \<Longrightarrow> a ^ (n - 1) * a = a ^ n"
+  by (simp add: power_commutes split add: nat_diff_split)
+
 end
 
 context comm_monoid_mult
@@ -584,6 +575,10 @@
   "a ^ n = b ^ n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < n \<Longrightarrow> a = b"
   by (cases n) (simp_all del: power_Suc, rule power_inject_base)
 
+lemma power_eq_iff_eq_base:
+  "0 < n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a ^ n = b ^ n \<longleftrightarrow> a = b"
+  using power_eq_imp_eq_base [of a n b] by auto
+
 lemma power2_le_imp_le:
   "x\<^sup>2 \<le> y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y"
   unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
@@ -596,6 +591,10 @@
   "x\<^sup>2 = y\<^sup>2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y"
   unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp
 
+lemma power_Suc_le_self:
+  shows "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ Suc n \<le> a"
+  using power_decreasing [of 1 "Suc n" a] by simp
+
 end
 
 context linordered_ring_strict
diff -r 97f2ed240431 -r 2230b7047376 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/Real.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -1037,9 +1037,6 @@
 declare of_int_1_less_iff [algebra, presburger]
 declare of_int_1_le_iff [algebra, presburger]
 
-lemma of_int_abs [simp]: "of_int \<bar>x\<bar> = (\<bar>of_int x\<bar> :: 'a::linordered_idom)"
-  by (auto simp add: abs_if)
-
 lemma int_less_real_le: "(n < m) = (real_of_int n + 1 <= real_of_int m)"
 proof -
   have "(0::real) \<le> 1"
@@ -1309,22 +1306,9 @@
 
 subsection \<open>Lemmas about powers\<close>
 
-(* used by Import/HOL/real.imp *)
 lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n"
   by simp
 
-text \<open>FIXME: no longer real-specific; rename and move elsewhere\<close>
-lemma realpow_Suc_le_self:
-  fixes r :: "'a::linordered_semidom"
-  shows "[| 0 \<le> r; r \<le> 1 |] ==> r ^ Suc n \<le> r"
-by (insert power_decreasing [of 1 "Suc n" r], simp)
-
-text \<open>FIXME: no longer real-specific; rename and move elsewhere\<close>
-lemma realpow_minus_mult:
-  fixes x :: "'a::monoid_mult"
-  shows "0 < n \<Longrightarrow> x ^ (n - 1) * x = x ^ n"
-by (simp add: power_Suc power_commutes split add: nat_diff_split)
-
 text \<open>FIXME: declare this [simp] for all types, or not at all\<close>
 declare sum_squares_eq_zero_iff [simp] sum_power2_eq_zero_iff [simp]
 
diff -r 97f2ed240431 -r 2230b7047376 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -9,9 +9,6 @@
 imports Real Topological_Spaces
 begin
 
-lemma (in ordered_ab_group_add) diff_ge_0_iff_ge [simp]: "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
-  by (simp add: le_diff_eq)
-
 subsection \<open>Locale for additive functions\<close>
 
 locale additive =
diff -r 97f2ed240431 -r 2230b7047376 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/Rings.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -1562,6 +1562,14 @@
 proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
   by (auto simp add: abs_if split: split_if_asm)
 
+lemma sum_squares_ge_zero:
+  "0 \<le> x * x + y * y"
+  by (intro add_nonneg_nonneg zero_le_square)
+
+lemma not_sum_squares_lt_zero:
+  "\<not> x * x + y * y < 0"
+  by (simp add: not_less sum_squares_ge_zero)
+
 end
 
 class linordered_ring_strict = ring + linordered_semiring_strict
@@ -1867,6 +1875,10 @@
   "sgn a < 0 \<longleftrightarrow> a < 0"
   unfolding sgn_if by auto
 
+lemma abs_sgn_eq:
+  "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
+  by (simp add: sgn_if)
+
 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
   by (simp add: abs_if)
 
diff -r 97f2ed240431 -r 2230b7047376 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/Transcendental.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -29,27 +29,15 @@
 qed
 
 
-lemma of_int_leD: 
-  fixes x :: "'a :: linordered_idom"
-  shows "\<bar>of_int n\<bar> \<le> x \<Longrightarrow> n=0 \<or> x\<ge>1"
-  by (metis (no_types) le_less_trans not_less of_int_abs of_int_less_1_iff zabs_less_one_iff)
-
-lemma of_int_lessD: 
-  fixes x :: "'a :: linordered_idom"
-  shows "\<bar>of_int n\<bar> < x \<Longrightarrow> n=0 \<or> x>1"
-  by (metis less_le_trans not_less of_int_abs of_int_less_1_iff zabs_less_one_iff)
-
-lemma fact_in_Reals: "fact n \<in> \<real>" by (induction n) auto
+lemma fact_in_Reals: "fact n \<in> \<real>"
+  by (induction n) auto
+
+lemma of_real_fact [simp]: "of_real (fact n) = fact n"
+  by (metis of_nat_fact of_real_of_nat_eq)
 
 lemma pochhammer_of_real: "pochhammer (of_real x) n = of_real (pochhammer x n)"
   by (simp add: pochhammer_def)
 
-lemma of_real_fact [simp]: "of_real (fact n) = fact n"
-  by (metis of_nat_fact of_real_of_nat_eq)
-
-lemma of_int_fact [simp]: "of_int (fact n :: int) = fact n"
-  by (metis of_int_of_nat_eq of_nat_fact)
-
 lemma norm_fact [simp]:
   "norm (fact n :: 'a :: {real_normed_algebra_1}) = fact n"
 proof -