src/HOL/Power.thy
changeset 61649 268d88ec9087
parent 61531 ab2e862263e7
child 61694 6571c78c9667
     1.1 --- a/src/HOL/Power.thy	Thu Nov 12 11:22:26 2015 +0100
     1.2 +++ b/src/HOL/Power.thy	Fri Nov 13 12:27:13 2015 +0000
     1.3 @@ -175,7 +175,7 @@
     1.4  context semiring_1
     1.5  begin
     1.6  
     1.7 -lemma of_nat_power:
     1.8 +lemma of_nat_power [simp]:
     1.9    "of_nat (m ^ n) = of_nat m ^ n"
    1.10    by (induct n) (simp_all add: of_nat_mult)
    1.11  
    1.12 @@ -310,7 +310,7 @@
    1.13  lemma power_minus1_odd:
    1.14    "(- 1) ^ Suc (2*n) = -1"
    1.15    by simp
    1.16 -  
    1.17 +
    1.18  lemma power_minus_even [simp]:
    1.19    "(-a) ^ (2*n) = a ^ (2*n)"
    1.20    by (simp add: power_minus [of a])
    1.21 @@ -320,7 +320,7 @@
    1.22  context ring_1_no_zero_divisors
    1.23  begin
    1.24  
    1.25 -subclass semiring_1_no_zero_divisors .. 
    1.26 +subclass semiring_1_no_zero_divisors ..
    1.27  
    1.28  lemma power2_eq_1_iff:
    1.29    "a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
    1.30 @@ -377,7 +377,7 @@
    1.31    "(1 / a) ^ n = 1 / a ^ n"
    1.32    using power_inverse [of a] by (simp add: divide_inverse)
    1.33  
    1.34 -end  
    1.35 +end
    1.36  
    1.37  context field
    1.38  begin
    1.39 @@ -463,6 +463,10 @@
    1.40    qed
    1.41  qed
    1.42  
    1.43 +lemma of_nat_zero_less_power_iff [simp]:
    1.44 +  "of_nat x ^ n > 0 \<longleftrightarrow> x > 0 \<or> n = 0"
    1.45 +  by (induct n) auto
    1.46 +
    1.47  text\<open>Surely we can strengthen this? It holds for @{text "0<a<1"} too.\<close>
    1.48  lemma power_inject_exp [simp]:
    1.49    "1 < a \<Longrightarrow> a ^ m = a ^ n \<longleftrightarrow> m = n"
    1.50 @@ -491,7 +495,7 @@
    1.51  proof (induct N)
    1.52    case 0 then show ?case by simp
    1.53  next
    1.54 -  case (Suc N) then show ?case 
    1.55 +  case (Suc N) then show ?case
    1.56    apply (auto simp add: power_Suc_less less_Suc_eq)
    1.57    apply (subgoal_tac "a * a^N < 1 * a^n")
    1.58    apply simp
    1.59 @@ -505,7 +509,7 @@
    1.60  proof (induct N)
    1.61    case 0 then show ?case by simp
    1.62  next
    1.63 -  case (Suc N) then show ?case 
    1.64 +  case (Suc N) then show ?case
    1.65    apply (auto simp add: le_Suc_eq)
    1.66    apply (subgoal_tac "a * a^N \<le> 1 * a^n", simp)
    1.67    apply (rule mult_mono) apply auto
    1.68 @@ -522,7 +526,7 @@
    1.69  proof (induct N)
    1.70    case 0 then show ?case by simp
    1.71  next
    1.72 -  case (Suc N) then show ?case 
    1.73 +  case (Suc N) then show ?case
    1.74    apply (auto simp add: le_Suc_eq)
    1.75    apply (subgoal_tac "1 * a^n \<le> a * a^N", simp)
    1.76    apply (rule mult_mono) apply (auto simp add: order_trans [OF zero_le_one])
    1.77 @@ -539,7 +543,7 @@
    1.78  proof (induct N)
    1.79    case 0 then show ?case by simp
    1.80  next
    1.81 -  case (Suc N) then show ?case 
    1.82 +  case (Suc N) then show ?case
    1.83    apply (auto simp add: power_less_power_Suc less_Suc_eq)
    1.84    apply (subgoal_tac "1 * a^n < a * a^N", simp)
    1.85    apply (rule mult_strict_mono) apply (auto simp add: less_trans [OF zero_less_one] less_imp_le)
    1.86 @@ -552,7 +556,7 @@
    1.87  
    1.88  lemma power_strict_increasing_iff [simp]:
    1.89    "1 < b \<Longrightarrow> b ^ x < b ^ y \<longleftrightarrow> x < y"
    1.90 -by (blast intro: power_less_imp_less_exp power_strict_increasing) 
    1.91 +by (blast intro: power_less_imp_less_exp power_strict_increasing)
    1.92  
    1.93  lemma power_le_imp_le_base:
    1.94    assumes le: "a ^ Suc n \<le> b ^ Suc n"
    1.95 @@ -680,7 +684,7 @@
    1.96  lemma odd_0_le_power_imp_0_le:
    1.97    "0 \<le> a ^ Suc (2*n) \<Longrightarrow> 0 \<le> a"
    1.98    using odd_power_less_zero [of a n]
    1.99 -    by (force simp add: linorder_not_less [symmetric]) 
   1.100 +    by (force simp add: linorder_not_less [symmetric])
   1.101  
   1.102  lemma zero_le_even_power'[simp]:
   1.103    "0 \<le> a ^ (2*n)"
   1.104 @@ -689,7 +693,7 @@
   1.105      show ?case by simp
   1.106  next
   1.107    case (Suc n)
   1.108 -    have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
   1.109 +    have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
   1.110        by (simp add: ac_simps power_add power2_eq_square)
   1.111      thus ?case
   1.112        by (simp add: Suc zero_le_mult_iff)
   1.113 @@ -733,7 +737,7 @@
   1.114  
   1.115  lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> abs(x) = 1"
   1.116    by (auto simp add: abs_if power2_eq_1_iff)
   1.117 -  
   1.118 +
   1.119  lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> abs(x) < 1"
   1.120    using  abs_square_eq_1 [of x] abs_square_le_1 [of x]
   1.121    by (auto simp add: le_less)
   1.122 @@ -768,10 +772,10 @@
   1.123  
   1.124  lemmas zero_compare_simps =
   1.125      add_strict_increasing add_strict_increasing2 add_increasing
   1.126 -    zero_le_mult_iff zero_le_divide_iff 
   1.127 -    zero_less_mult_iff zero_less_divide_iff 
   1.128 -    mult_le_0_iff divide_le_0_iff 
   1.129 -    mult_less_0_iff divide_less_0_iff 
   1.130 +    zero_le_mult_iff zero_le_divide_iff
   1.131 +    zero_less_mult_iff zero_less_divide_iff
   1.132 +    mult_le_0_iff divide_le_0_iff
   1.133 +    mult_less_0_iff divide_less_0_iff
   1.134      zero_le_power2 power2_less_0
   1.135  
   1.136  
   1.137 @@ -785,7 +789,7 @@
   1.138    "x ^ n > 0 \<longleftrightarrow> x > (0::nat) \<or> n = 0"
   1.139    by (induct n) auto
   1.140  
   1.141 -lemma nat_power_eq_Suc_0_iff [simp]: 
   1.142 +lemma nat_power_eq_Suc_0_iff [simp]:
   1.143    "x ^ m = Suc 0 \<longleftrightarrow> m = 0 \<or> x = Suc 0"
   1.144    by (induct m) auto
   1.145  
   1.146 @@ -842,13 +846,13 @@
   1.147  
   1.148  lemma card_Pow: "finite A \<Longrightarrow> card (Pow A) = 2 ^ card A"
   1.149  proof (induct rule: finite_induct)
   1.150 -  case empty 
   1.151 +  case empty
   1.152      show ?case by auto
   1.153  next
   1.154    case (insert x A)
   1.155 -  then have "inj_on (insert x) (Pow A)" 
   1.156 +  then have "inj_on (insert x) (Pow A)"
   1.157      unfolding inj_on_def by (blast elim!: equalityE)
   1.158 -  then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A" 
   1.159 +  then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A"
   1.160      by (simp add: mult_2 card_image Pow_insert insert.hyps)
   1.161    then show ?case using insert
   1.162      apply (simp add: Pow_insert)
   1.163 @@ -882,11 +886,11 @@
   1.164  lemma setprod_power_distrib:
   1.165    fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1"
   1.166    shows "setprod f A ^ n = setprod (\<lambda>x. (f x) ^ n) A"
   1.167 -proof (cases "finite A") 
   1.168 -  case True then show ?thesis 
   1.169 +proof (cases "finite A")
   1.170 +  case True then show ?thesis
   1.171      by (induct A rule: finite_induct) (auto simp add: power_mult_distrib)
   1.172  next
   1.173 -  case False then show ?thesis 
   1.174 +  case False then show ?thesis
   1.175      by simp
   1.176  qed
   1.177  
   1.178 @@ -902,13 +906,13 @@
   1.179    {assume a: "a \<notin> S"
   1.180      hence "\<forall> k\<in> S. ?f k = c" by simp
   1.181      hence ?thesis  using a setprod_constant[OF fS, of c] by simp }
   1.182 -  moreover 
   1.183 +  moreover
   1.184    {assume a: "a \<in> S"
   1.185      let ?A = "S - {a}"
   1.186      let ?B = "{a}"
   1.187 -    have eq: "S = ?A \<union> ?B" using a by blast 
   1.188 +    have eq: "S = ?A \<union> ?B" using a by blast
   1.189      have dj: "?A \<inter> ?B = {}" by simp
   1.190 -    from fS have fAB: "finite ?A" "finite ?B" by auto  
   1.191 +    from fS have fAB: "finite ?A" "finite ?B" by auto
   1.192      have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
   1.193        apply (rule setprod.cong) by auto
   1.194      have cA: "card ?A = card S - 1" using fS a by auto