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.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.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 *)"
```