src/HOL/Power.thy
changeset 60758 d8d85a8172b5
parent 60685 cb21b7022b00
child 60866 7f562aa4eb4b
     1.1 --- a/src/HOL/Power.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Power.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -3,13 +3,13 @@
     1.4      Copyright   1997  University of Cambridge
     1.5  *)
     1.6  
     1.7 -section {* Exponentiation *}
     1.8 +section \<open>Exponentiation\<close>
     1.9  
    1.10  theory Power
    1.11  imports Num Equiv_Relations
    1.12  begin
    1.13  
    1.14 -subsection {* Powers for Arbitrary Monoids *}
    1.15 +subsection \<open>Powers for Arbitrary Monoids\<close>
    1.16  
    1.17  class power = one + times
    1.18  begin
    1.19 @@ -24,7 +24,7 @@
    1.20  notation (HTML output)
    1.21    power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
    1.22  
    1.23 -text {* Special syntax for squares. *}
    1.24 +text \<open>Special syntax for squares.\<close>
    1.25  
    1.26  abbreviation (xsymbols)
    1.27    power2 :: "'a \<Rightarrow> 'a"  ("(_\<^sup>2)" [1000] 999) where
    1.28 @@ -131,7 +131,7 @@
    1.29  
    1.30  end
    1.31  
    1.32 -text{*Extract constant factors from powers*}
    1.33 +text\<open>Extract constant factors from powers\<close>
    1.34  declare power_mult_distrib [where a = "numeral w" for w, simp]
    1.35  declare power_mult_distrib [where b = "numeral w" for w, simp]
    1.36  
    1.37 @@ -191,13 +191,13 @@
    1.38  context comm_semiring_1
    1.39  begin
    1.40  
    1.41 -text {* The divides relation *}
    1.42 +text \<open>The divides relation\<close>
    1.43  
    1.44  lemma le_imp_power_dvd:
    1.45    assumes "m \<le> n" shows "a ^ m dvd a ^ n"
    1.46  proof
    1.47    have "a ^ n = a ^ (m + (n - m))"
    1.48 -    using `m \<le> n` by simp
    1.49 +    using \<open>m \<le> n\<close> by simp
    1.50    also have "\<dots> = a ^ m * a ^ (n - m)"
    1.51      by (rule power_add)
    1.52    finally show "a ^ n = a ^ m * a ^ (n - m)" .
    1.53 @@ -322,7 +322,7 @@
    1.54  context division_ring
    1.55  begin
    1.56  
    1.57 -text {* FIXME reorient or rename to @{text nonzero_inverse_power} *}
    1.58 +text \<open>FIXME reorient or rename to @{text nonzero_inverse_power}\<close>
    1.59  lemma nonzero_power_inverse:
    1.60    "a \<noteq> 0 \<Longrightarrow> inverse (a ^ n) = (inverse a) ^ n"
    1.61    by (induct n)
    1.62 @@ -342,7 +342,7 @@
    1.63  end
    1.64  
    1.65  
    1.66 -subsection {* Exponentiation on ordered types *}
    1.67 +subsection \<open>Exponentiation on ordered types\<close>
    1.68  
    1.69  context linordered_ring (* TODO: move *)
    1.70  begin
    1.71 @@ -386,7 +386,7 @@
    1.72      by (fact order_trans [OF zero_le_one less_imp_le])
    1.73    have "1 * 1 < a * 1" using gt1 by simp
    1.74    also have "\<dots> \<le> a * a ^ n" using gt1
    1.75 -    by (simp only: mult_mono `0 \<le> a` one_le_power order_less_imp_le
    1.76 +    by (simp only: mult_mono \<open>0 \<le> a\<close> one_le_power order_less_imp_le
    1.77          zero_le_one order_refl)
    1.78    finally show ?thesis by simp
    1.79  qed
    1.80 @@ -422,13 +422,13 @@
    1.81    qed
    1.82  qed
    1.83  
    1.84 -text{*Surely we can strengthen this? It holds for @{text "0<a<1"} too.*}
    1.85 +text\<open>Surely we can strengthen this? It holds for @{text "0<a<1"} too.\<close>
    1.86  lemma power_inject_exp [simp]:
    1.87    "1 < a \<Longrightarrow> a ^ m = a ^ n \<longleftrightarrow> m = n"
    1.88    by (force simp add: order_antisym power_le_imp_le_exp)
    1.89  
    1.90 -text{*Can relax the first premise to @{term "0<a"} in the case of the
    1.91 -natural numbers.*}
    1.92 +text\<open>Can relax the first premise to @{term "0<a"} in the case of the
    1.93 +natural numbers.\<close>
    1.94  lemma power_less_imp_less_exp:
    1.95    "1 < a \<Longrightarrow> a ^ m < a ^ n \<Longrightarrow> m < n"
    1.96    by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"]
    1.97 @@ -439,7 +439,7 @@
    1.98    by (induct n)
    1.99     (auto simp add: mult_strict_mono le_less_trans [of 0 a b])
   1.100  
   1.101 -text{*Lemma for @{text power_strict_decreasing}*}
   1.102 +text\<open>Lemma for @{text power_strict_decreasing}\<close>
   1.103  lemma power_Suc_less:
   1.104    "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n"
   1.105    by (induct n)
   1.106 @@ -458,7 +458,7 @@
   1.107    done
   1.108  qed
   1.109  
   1.110 -text{*Proof resembles that of @{text power_strict_decreasing}*}
   1.111 +text\<open>Proof resembles that of @{text power_strict_decreasing}\<close>
   1.112  lemma power_decreasing [rule_format]:
   1.113    "n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<longrightarrow> a ^ N \<le> a ^ n"
   1.114  proof (induct N)
   1.115 @@ -475,7 +475,7 @@
   1.116    "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1"
   1.117    using power_strict_decreasing [of 0 "Suc n" a] by simp
   1.118  
   1.119 -text{*Proof again resembles that of @{text power_strict_decreasing}*}
   1.120 +text\<open>Proof again resembles that of @{text power_strict_decreasing}\<close>
   1.121  lemma power_increasing [rule_format]:
   1.122    "n \<le> N \<Longrightarrow> 1 \<le> a \<Longrightarrow> a ^ n \<le> a ^ N"
   1.123  proof (induct N)
   1.124 @@ -488,7 +488,7 @@
   1.125    done
   1.126  qed
   1.127  
   1.128 -text{*Lemma for @{text power_strict_increasing}*}
   1.129 +text\<open>Lemma for @{text power_strict_increasing}\<close>
   1.130  lemma power_less_power_Suc:
   1.131    "1 < a \<Longrightarrow> a ^ n < a * a ^ n"
   1.132    by (induct n) (auto simp add: mult_strict_left_mono less_trans [OF zero_less_one])
   1.133 @@ -700,7 +700,7 @@
   1.134  end
   1.135  
   1.136  
   1.137 -subsection {* Miscellaneous rules *}
   1.138 +subsection \<open>Miscellaneous rules\<close>
   1.139  
   1.140  lemma self_le_power:
   1.141    fixes x::"'a::linordered_semidom" 
   1.142 @@ -722,7 +722,7 @@
   1.143    "(0::'a::{power, semiring_0}) ^ Suc n = 0"
   1.144    by simp
   1.145  
   1.146 -text{*It looks plausible as a simprule, but its effect can be strange.*}
   1.147 +text\<open>It looks plausible as a simprule, but its effect can be strange.\<close>
   1.148  lemma power_0_left:
   1.149    "0 ^ n = (if n = 0 then 1 else (0::'a::{power, semiring_0}))"
   1.150    by (induct n) simp_all
   1.151 @@ -732,7 +732,7 @@
   1.152    shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
   1.153    by (induct m n rule: diff_induct) (simp_all add: nz field_power_not_zero)
   1.154  
   1.155 -text{*Perhaps these should be simprules.*}
   1.156 +text\<open>Perhaps these should be simprules.\<close>
   1.157  lemma power_inverse:
   1.158    fixes a :: "'a::division_ring"
   1.159    shows "inverse (a ^ n) = inverse a ^ n"
   1.160 @@ -753,7 +753,7 @@
   1.161  apply assumption
   1.162  done
   1.163  
   1.164 -text {* Simprules for comparisons where common factors can be cancelled. *}
   1.165 +text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
   1.166  
   1.167  lemmas zero_compare_simps =
   1.168      add_strict_increasing add_strict_increasing2 add_increasing
   1.169 @@ -764,7 +764,7 @@
   1.170      zero_le_power2 power2_less_0
   1.171  
   1.172  
   1.173 -subsection {* Exponentiation for the Natural Numbers *}
   1.174 +subsection \<open>Exponentiation for the Natural Numbers\<close>
   1.175  
   1.176  lemma nat_one_le_power [simp]:
   1.177    "Suc 0 \<le> i \<Longrightarrow> Suc 0 \<le> i ^ n"
   1.178 @@ -782,9 +782,9 @@
   1.179    "Suc 0 ^ n = Suc 0"
   1.180    by simp
   1.181  
   1.182 -text{*Valid for the naturals, but what if @{text"0<i<1"}?
   1.183 +text\<open>Valid for the naturals, but what if @{text"0<i<1"}?
   1.184  Premises cannot be weakened: consider the case where @{term "i=0"},
   1.185 -@{term "m=1"} and @{term "n=0"}.*}
   1.186 +@{term "m=1"} and @{term "n=0"}.\<close>
   1.187  lemma nat_power_less_imp_less:
   1.188    assumes nonneg: "0 < (i\<Colon>nat)"
   1.189    assumes less: "i ^ m < i ^ n"
   1.190 @@ -824,7 +824,7 @@
   1.191    qed
   1.192  qed
   1.193  
   1.194 -subsubsection {* Cardinality of the Powerset *}
   1.195 +subsubsection \<open>Cardinality of the Powerset\<close>
   1.196  
   1.197  lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2"
   1.198    unfolding UNIV_bool by simp
   1.199 @@ -846,7 +846,7 @@
   1.200  qed
   1.201  
   1.202  
   1.203 -subsubsection {* Generalized sum over a set *}
   1.204 +subsubsection \<open>Generalized sum over a set\<close>
   1.205  
   1.206  lemma setsum_zero_power [simp]:
   1.207    fixes c :: "nat \<Rightarrow> 'a::division_ring"
   1.208 @@ -861,7 +861,7 @@
   1.209    by auto
   1.210  
   1.211  
   1.212 -subsubsection {* Generalized product over a set *}
   1.213 +subsubsection \<open>Generalized product over a set\<close>
   1.214  
   1.215  lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
   1.216  apply (erule finite_induct)
   1.217 @@ -910,7 +910,7 @@
   1.218    ultimately show ?thesis by blast
   1.219  qed
   1.220  
   1.221 -subsection {* Code generator tweak *}
   1.222 +subsection \<open>Code generator tweak\<close>
   1.223  
   1.224  lemma power_power_power [code]:
   1.225    "power = power.power (1::'a::{power}) (op *)"