generalized some lemmas;
authorhaftmann
Wed Feb 17 21:51:57 2016 +0100 (2016-02-17)
changeset 623472230b7047376
parent 62346 97f2ed240431
child 62348 9a5f43dac883
generalized some lemmas;
moved some lemmas in more appropriate places;
deleted potentially dangerous simp rule
NEWS
src/HOL/Algebra/Coset.thy
src/HOL/Binomial.thy
src/HOL/Fields.thy
src/HOL/GCD.thy
src/HOL/Groups.thy
src/HOL/Int.thy
src/HOL/NthRoot.thy
src/HOL/Power.thy
src/HOL/Real.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Rings.thy
src/HOL/Transcendental.thy
     1.1 --- a/NEWS	Wed Feb 17 21:51:56 2016 +0100
     1.2 +++ b/NEWS	Wed Feb 17 21:51:57 2016 +0100
     1.3 @@ -37,6 +37,11 @@
     1.4  
     1.5  * Class semiring_Lcd merged into semiring_Gcd.  INCOMPATIBILITY.
     1.6  
     1.7 +* Lemma generalization:
     1.8 +    realpow_minus_mult ~> power_minus_mult
     1.9 +    realpow_Suc_le_self ~> power_Suc_le_self
    1.10 +INCOMPATIBILITY.
    1.11 +
    1.12  
    1.13  New in Isabelle2016 (February 2016)
    1.14  -----------------------------------
     2.1 --- a/src/HOL/Algebra/Coset.thy	Wed Feb 17 21:51:56 2016 +0100
     2.2 +++ b/src/HOL/Algebra/Coset.thy	Wed Feb 17 21:51:57 2016 +0100
     2.3 @@ -936,18 +936,6 @@
     2.4    thus ?thesis by (auto simp add: g)
     2.5  qed
     2.6  
     2.7 -lemma the_elem_image_unique: -- {* FIXME move *}
     2.8 -  assumes "A \<noteq> {}"
     2.9 -  assumes *: "\<And>y. y \<in> A \<Longrightarrow> f y = f x"
    2.10 -  shows "the_elem (f ` A) = f x"
    2.11 -unfolding the_elem_def proof (rule the1_equality)
    2.12 -  from `A \<noteq> {}` obtain y where "y \<in> A" by auto
    2.13 -  with * have "f x = f y" by simp
    2.14 -  with `y \<in> A` have "f x \<in> f ` A" by blast
    2.15 -  with * show "f ` A = {f x}" by auto
    2.16 -  then show "\<exists>!x. f ` A = {x}" by auto
    2.17 -qed
    2.18 -
    2.19  lemma (in group_hom) FactGroup_hom:
    2.20       "(\<lambda>X. the_elem (h`X)) \<in> hom (G Mod (kernel G H h)) H"
    2.21  apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
     3.1 --- a/src/HOL/Binomial.thy	Wed Feb 17 21:51:56 2016 +0100
     3.2 +++ b/src/HOL/Binomial.thy	Wed Feb 17 21:51:57 2016 +0100
     3.3 @@ -25,9 +25,19 @@
     3.4  lemma fact_Suc_0 [simp]: "fact (Suc 0) = Suc 0"
     3.5    by simp
     3.6  
     3.7 -lemma of_nat_fact [simp]: "of_nat (fact n) = fact n"
     3.8 +lemma of_nat_fact [simp]:
     3.9 +  "of_nat (fact n) = fact n"
    3.10    by (induct n) (auto simp add: algebra_simps of_nat_mult)
    3.11   
    3.12 +lemma of_int_fact [simp]:
    3.13 +  "of_int (fact n) = fact n"
    3.14 +proof -
    3.15 +  have "of_int (of_nat (fact n)) = fact n"
    3.16 +    unfolding of_int_of_nat_eq by simp
    3.17 +  then show ?thesis
    3.18 +    by simp
    3.19 +qed
    3.20 +
    3.21  lemma fact_reduce: "n > 0 \<Longrightarrow> fact n = of_nat n * fact (n - 1)"
    3.22    by (cases n) auto
    3.23  
     4.1 --- a/src/HOL/Fields.thy	Wed Feb 17 21:51:56 2016 +0100
     4.2 +++ b/src/HOL/Fields.thy	Wed Feb 17 21:51:57 2016 +0100
     4.3 @@ -1152,6 +1152,10 @@
     4.4  lemma divide_le_0_abs_iff [simp]: "(a / \<bar>b\<bar> \<le> 0) = (a \<le> 0 | b = 0)"
     4.5  by (auto simp: divide_le_0_iff)
     4.6  
     4.7 +lemma inverse_sgn:
     4.8 +  "sgn (inverse a) = inverse (sgn a)"
     4.9 +  by (simp add: sgn_if)
    4.10 +
    4.11  lemma field_le_mult_one_interval:
    4.12    assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
    4.13    shows "x \<le> y"
     5.1 --- a/src/HOL/GCD.thy	Wed Feb 17 21:51:56 2016 +0100
     5.2 +++ b/src/HOL/GCD.thy	Wed Feb 17 21:51:57 2016 +0100
     5.3 @@ -2057,9 +2057,6 @@
     5.4  
     5.5  text \<open>Fact aliasses\<close>
     5.6  
     5.7 -lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat \<bar>x\<bar> dvd nat \<bar>y\<bar>"
     5.8 -  by (fact dvd_int_unfold_dvd_nat)
     5.9 -
    5.10  lemmas gcd_assoc_nat = gcd.assoc [where ?'a = nat]
    5.11  lemmas gcd_assoc_int = gcd.assoc [where ?'a = int]
    5.12  lemmas gcd_commute_nat = gcd.commute [where ?'a = nat]
     6.1 --- a/src/HOL/Groups.thy	Wed Feb 17 21:51:56 2016 +0100
     6.2 +++ b/src/HOL/Groups.thy	Wed Feb 17 21:51:57 2016 +0100
     6.3 @@ -1382,7 +1382,6 @@
     6.4  lemmas ab_left_minus = left_minus \<comment> \<open>FIXME duplicate\<close>
     6.5  lemmas diff_diff_eq = diff_diff_add \<comment> \<open>FIXME duplicate\<close>
     6.6  
     6.7 -
     6.8  subsection \<open>Tools setup\<close>
     6.9  
    6.10  lemma add_mono_thms_linordered_semiring:
     7.1 --- a/src/HOL/Int.thy	Wed Feb 17 21:51:56 2016 +0100
     7.2 +++ b/src/HOL/Int.thy	Wed Feb 17 21:51:57 2016 +0100
     7.3 @@ -190,6 +190,21 @@
     7.4  apply arith
     7.5  done
     7.6  
     7.7 +lemma zabs_less_one_iff [simp]:
     7.8 +  fixes z :: int
     7.9 +  shows "\<bar>z\<bar> < 1 \<longleftrightarrow> z = 0" (is "?P \<longleftrightarrow> ?Q")
    7.10 +proof
    7.11 +  assume ?Q then show ?P by simp
    7.12 +next
    7.13 +  assume ?P
    7.14 +  with zless_imp_add1_zle [of "\<bar>z\<bar>" 1] have "\<bar>z\<bar> + 1 \<le> 1"
    7.15 +    by simp
    7.16 +  then have "\<bar>z\<bar> \<le> 0"
    7.17 +    by simp
    7.18 +  then show ?Q
    7.19 +    by simp
    7.20 +qed
    7.21 +
    7.22  lemmas int_distrib =
    7.23    distrib_right [of z1 z2 w]
    7.24    distrib_left [of w z1 z2]
    7.25 @@ -320,6 +335,45 @@
    7.26  lemma of_int_nonneg: "z \<ge> 0 \<Longrightarrow> of_int z \<ge> 0"
    7.27    by simp
    7.28  
    7.29 +lemma of_int_abs [simp]:
    7.30 +  "of_int \<bar>x\<bar> = \<bar>of_int x\<bar>"
    7.31 +  by (auto simp add: abs_if)
    7.32 +
    7.33 +lemma of_int_lessD:
    7.34 +  assumes "\<bar>of_int n\<bar> < x"
    7.35 +  shows "n = 0 \<or> x > 1"
    7.36 +proof (cases "n = 0")
    7.37 +  case True then show ?thesis by simp
    7.38 +next
    7.39 +  case False
    7.40 +  then have "\<bar>n\<bar> \<noteq> 0" by simp
    7.41 +  then have "\<bar>n\<bar> > 0" by simp
    7.42 +  then have "\<bar>n\<bar> \<ge> 1"
    7.43 +    using zless_imp_add1_zle [of 0 "\<bar>n\<bar>"] by simp
    7.44 +  then have "\<bar>of_int n\<bar> \<ge> 1"
    7.45 +    unfolding of_int_1_le_iff [of "\<bar>n\<bar>", symmetric] by simp
    7.46 +  then have "1 < x" using assms by (rule le_less_trans)
    7.47 +  then show ?thesis ..
    7.48 +qed
    7.49 +
    7.50 +lemma of_int_leD:
    7.51 +  assumes "\<bar>of_int n\<bar> \<le> x"
    7.52 +  shows "n = 0 \<or> 1 \<le> x"
    7.53 +proof (cases "n = 0")
    7.54 +  case True then show ?thesis by simp
    7.55 +next
    7.56 +  case False
    7.57 +  then have "\<bar>n\<bar> \<noteq> 0" by simp
    7.58 +  then have "\<bar>n\<bar> > 0" by simp
    7.59 +  then have "\<bar>n\<bar> \<ge> 1"
    7.60 +    using zless_imp_add1_zle [of 0 "\<bar>n\<bar>"] by simp
    7.61 +  then have "\<bar>of_int n\<bar> \<ge> 1"
    7.62 +    unfolding of_int_1_le_iff [of "\<bar>n\<bar>", symmetric] by simp
    7.63 +  then have "1 \<le> x" using assms by (rule order_trans)
    7.64 +  then show ?thesis ..
    7.65 +qed
    7.66 +
    7.67 +
    7.68  end
    7.69  
    7.70  text \<open>Comparisons involving @{term of_int}.\<close>
    7.71 @@ -1152,9 +1206,6 @@
    7.72  
    7.73  subsection\<open>Products and 1, by T. M. Rasmussen\<close>
    7.74  
    7.75 -lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
    7.76 -by arith
    7.77 -
    7.78  lemma abs_zmult_eq_1:
    7.79    assumes mn: "\<bar>m * n\<bar> = 1"
    7.80    shows "\<bar>m\<bar> = (1::int)"
     8.1 --- a/src/HOL/NthRoot.thy	Wed Feb 17 21:51:56 2016 +0100
     8.2 +++ b/src/HOL/NthRoot.thy	Wed Feb 17 21:51:57 2016 +0100
     8.3 @@ -10,17 +10,6 @@
     8.4  imports Deriv Binomial
     8.5  begin
     8.6  
     8.7 -lemma abs_sgn_eq: "\<bar>sgn x :: real\<bar> = (if x = 0 then 0 else 1)"
     8.8 -  by (simp add: sgn_real_def)
     8.9 -
    8.10 -lemma inverse_sgn: "sgn (inverse a) = inverse (sgn a :: real)"
    8.11 -  by (simp add: sgn_real_def)
    8.12 -
    8.13 -lemma power_eq_iff_eq_base:
    8.14 -  fixes a b :: "_ :: linordered_semidom"
    8.15 -  shows "0 < n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a ^ n = b ^ n \<longleftrightarrow> a = b"
    8.16 -  using power_eq_imp_eq_base[of a n b] by auto
    8.17 -
    8.18  subsection \<open>Existence of Nth Root\<close>
    8.19  
    8.20  text \<open>Existence follows from the Intermediate Value Theorem\<close>
     9.1 --- a/src/HOL/Power.thy	Wed Feb 17 21:51:56 2016 +0100
     9.2 +++ b/src/HOL/Power.thy	Wed Feb 17 21:51:57 2016 +0100
     9.3 @@ -9,19 +9,6 @@
     9.4  imports Num Equiv_Relations
     9.5  begin
     9.6  
     9.7 -context linordered_ring (* TODO: move *)
     9.8 -begin
     9.9 -
    9.10 -lemma sum_squares_ge_zero:
    9.11 -  "0 \<le> x * x + y * y"
    9.12 -  by (intro add_nonneg_nonneg zero_le_square)
    9.13 -
    9.14 -lemma not_sum_squares_lt_zero:
    9.15 -  "\<not> x * x + y * y < 0"
    9.16 -  by (simp add: not_less sum_squares_ge_zero)
    9.17 -
    9.18 -end
    9.19 -
    9.20  subsection \<open>Powers for Arbitrary Monoids\<close>
    9.21  
    9.22  class power = one + times
    9.23 @@ -123,6 +110,10 @@
    9.24    finally show ?case .
    9.25  qed simp
    9.26  
    9.27 +lemma power_minus_mult:
    9.28 +  "0 < n \<Longrightarrow> a ^ (n - 1) * a = a ^ n"
    9.29 +  by (simp add: power_commutes split add: nat_diff_split)
    9.30 +
    9.31  end
    9.32  
    9.33  context comm_monoid_mult
    9.34 @@ -584,6 +575,10 @@
    9.35    "a ^ n = b ^ n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < n \<Longrightarrow> a = b"
    9.36    by (cases n) (simp_all del: power_Suc, rule power_inject_base)
    9.37  
    9.38 +lemma power_eq_iff_eq_base:
    9.39 +  "0 < n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a ^ n = b ^ n \<longleftrightarrow> a = b"
    9.40 +  using power_eq_imp_eq_base [of a n b] by auto
    9.41 +
    9.42  lemma power2_le_imp_le:
    9.43    "x\<^sup>2 \<le> y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y"
    9.44    unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
    9.45 @@ -596,6 +591,10 @@
    9.46    "x\<^sup>2 = y\<^sup>2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y"
    9.47    unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp
    9.48  
    9.49 +lemma power_Suc_le_self:
    9.50 +  shows "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ Suc n \<le> a"
    9.51 +  using power_decreasing [of 1 "Suc n" a] by simp
    9.52 +
    9.53  end
    9.54  
    9.55  context linordered_ring_strict
    10.1 --- a/src/HOL/Real.thy	Wed Feb 17 21:51:56 2016 +0100
    10.2 +++ b/src/HOL/Real.thy	Wed Feb 17 21:51:57 2016 +0100
    10.3 @@ -1037,9 +1037,6 @@
    10.4  declare of_int_1_less_iff [algebra, presburger]
    10.5  declare of_int_1_le_iff [algebra, presburger]
    10.6  
    10.7 -lemma of_int_abs [simp]: "of_int \<bar>x\<bar> = (\<bar>of_int x\<bar> :: 'a::linordered_idom)"
    10.8 -  by (auto simp add: abs_if)
    10.9 -
   10.10  lemma int_less_real_le: "(n < m) = (real_of_int n + 1 <= real_of_int m)"
   10.11  proof -
   10.12    have "(0::real) \<le> 1"
   10.13 @@ -1309,22 +1306,9 @@
   10.14  
   10.15  subsection \<open>Lemmas about powers\<close>
   10.16  
   10.17 -(* used by Import/HOL/real.imp *)
   10.18  lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n"
   10.19    by simp
   10.20  
   10.21 -text \<open>FIXME: no longer real-specific; rename and move elsewhere\<close>
   10.22 -lemma realpow_Suc_le_self:
   10.23 -  fixes r :: "'a::linordered_semidom"
   10.24 -  shows "[| 0 \<le> r; r \<le> 1 |] ==> r ^ Suc n \<le> r"
   10.25 -by (insert power_decreasing [of 1 "Suc n" r], simp)
   10.26 -
   10.27 -text \<open>FIXME: no longer real-specific; rename and move elsewhere\<close>
   10.28 -lemma realpow_minus_mult:
   10.29 -  fixes x :: "'a::monoid_mult"
   10.30 -  shows "0 < n \<Longrightarrow> x ^ (n - 1) * x = x ^ n"
   10.31 -by (simp add: power_Suc power_commutes split add: nat_diff_split)
   10.32 -
   10.33  text \<open>FIXME: declare this [simp] for all types, or not at all\<close>
   10.34  declare sum_squares_eq_zero_iff [simp] sum_power2_eq_zero_iff [simp]
   10.35  
    11.1 --- a/src/HOL/Real_Vector_Spaces.thy	Wed Feb 17 21:51:56 2016 +0100
    11.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Feb 17 21:51:57 2016 +0100
    11.3 @@ -9,9 +9,6 @@
    11.4  imports Real Topological_Spaces
    11.5  begin
    11.6  
    11.7 -lemma (in ordered_ab_group_add) diff_ge_0_iff_ge [simp]: "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
    11.8 -  by (simp add: le_diff_eq)
    11.9 -
   11.10  subsection \<open>Locale for additive functions\<close>
   11.11  
   11.12  locale additive =
    12.1 --- a/src/HOL/Rings.thy	Wed Feb 17 21:51:56 2016 +0100
    12.2 +++ b/src/HOL/Rings.thy	Wed Feb 17 21:51:57 2016 +0100
    12.3 @@ -1562,6 +1562,14 @@
    12.4  proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
    12.5    by (auto simp add: abs_if split: split_if_asm)
    12.6  
    12.7 +lemma sum_squares_ge_zero:
    12.8 +  "0 \<le> x * x + y * y"
    12.9 +  by (intro add_nonneg_nonneg zero_le_square)
   12.10 +
   12.11 +lemma not_sum_squares_lt_zero:
   12.12 +  "\<not> x * x + y * y < 0"
   12.13 +  by (simp add: not_less sum_squares_ge_zero)
   12.14 +
   12.15  end
   12.16  
   12.17  class linordered_ring_strict = ring + linordered_semiring_strict
   12.18 @@ -1867,6 +1875,10 @@
   12.19    "sgn a < 0 \<longleftrightarrow> a < 0"
   12.20    unfolding sgn_if by auto
   12.21  
   12.22 +lemma abs_sgn_eq:
   12.23 +  "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
   12.24 +  by (simp add: sgn_if)
   12.25 +
   12.26  lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
   12.27    by (simp add: abs_if)
   12.28  
    13.1 --- a/src/HOL/Transcendental.thy	Wed Feb 17 21:51:56 2016 +0100
    13.2 +++ b/src/HOL/Transcendental.thy	Wed Feb 17 21:51:57 2016 +0100
    13.3 @@ -29,27 +29,15 @@
    13.4  qed
    13.5  
    13.6  
    13.7 -lemma of_int_leD: 
    13.8 -  fixes x :: "'a :: linordered_idom"
    13.9 -  shows "\<bar>of_int n\<bar> \<le> x \<Longrightarrow> n=0 \<or> x\<ge>1"
   13.10 -  by (metis (no_types) le_less_trans not_less of_int_abs of_int_less_1_iff zabs_less_one_iff)
   13.11 -
   13.12 -lemma of_int_lessD: 
   13.13 -  fixes x :: "'a :: linordered_idom"
   13.14 -  shows "\<bar>of_int n\<bar> < x \<Longrightarrow> n=0 \<or> x>1"
   13.15 -  by (metis less_le_trans not_less of_int_abs of_int_less_1_iff zabs_less_one_iff)
   13.16 -
   13.17 -lemma fact_in_Reals: "fact n \<in> \<real>" by (induction n) auto
   13.18 +lemma fact_in_Reals: "fact n \<in> \<real>"
   13.19 +  by (induction n) auto
   13.20 +
   13.21 +lemma of_real_fact [simp]: "of_real (fact n) = fact n"
   13.22 +  by (metis of_nat_fact of_real_of_nat_eq)
   13.23  
   13.24  lemma pochhammer_of_real: "pochhammer (of_real x) n = of_real (pochhammer x n)"
   13.25    by (simp add: pochhammer_def)
   13.26  
   13.27 -lemma of_real_fact [simp]: "of_real (fact n) = fact n"
   13.28 -  by (metis of_nat_fact of_real_of_nat_eq)
   13.29 -
   13.30 -lemma of_int_fact [simp]: "of_int (fact n :: int) = fact n"
   13.31 -  by (metis of_int_of_nat_eq of_nat_fact)
   13.32 -
   13.33  lemma norm_fact [simp]:
   13.34    "norm (fact n :: 'a :: {real_normed_algebra_1}) = fact n"
   13.35  proof -