src/HOL/Int.thy
 changeset 60758 d8d85a8172b5 parent 60570 7ed2cde6806d child 60868 dd18c33c001e
```     1.1 --- a/src/HOL/Int.thy	Sat Jul 18 21:44:18 2015 +0200
1.2 +++ b/src/HOL/Int.thy	Sat Jul 18 22:58:50 2015 +0200
1.3 @@ -3,13 +3,13 @@
1.4      Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
1.5  *)
1.6
1.7 -section {* The Integers as Equivalence Classes over Pairs of Natural Numbers *}
1.8 +section \<open>The Integers as Equivalence Classes over Pairs of Natural Numbers\<close>
1.9
1.10  theory Int
1.11  imports Equiv_Relations Power Quotient Fun_Def
1.12  begin
1.13
1.14 -subsection {* Definition of integers as a quotient type *}
1.15 +subsection \<open>Definition of integers as a quotient type\<close>
1.16
1.17  definition intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" where
1.18    "intrel = (\<lambda>(x, y) (u, v). x + v = u + y)"
1.19 @@ -32,7 +32,7 @@
1.20       "(!!x y. z = Abs_Integ (x, y) ==> P) ==> P"
1.21  by (induct z) auto
1.22
1.23 -subsection {* Integers form a commutative ring *}
1.24 +subsection \<open>Integers form a commutative ring\<close>
1.25
1.26  instantiation int :: comm_ring_1
1.27  begin
1.28 @@ -85,7 +85,7 @@
1.29    obtains (diff) m n where "z = int m - int n"
1.30    by transfer clarsimp
1.31
1.32 -subsection {* Integers are totally ordered *}
1.33 +subsection \<open>Integers are totally ordered\<close>
1.34
1.35  instantiation int :: linorder
1.36  begin
1.37 @@ -118,7 +118,7 @@
1.38
1.39  end
1.40
1.41 -subsection {* Ordering properties of arithmetic operations *}
1.42 +subsection \<open>Ordering properties of arithmetic operations\<close>
1.43
1.45  proof
1.46 @@ -127,9 +127,9 @@
1.47      by transfer clarsimp
1.48  qed
1.49
1.50 -text{*Strict Monotonicity of Multiplication*}
1.51 +text\<open>Strict Monotonicity of Multiplication\<close>
1.52
1.53 -text{*strict, in 1st argument; proof is by induction on k>0*}
1.54 +text\<open>strict, in 1st argument; proof is by induction on k>0\<close>
1.55  lemma zmult_zless_mono2_lemma:
1.56       "(i::int)<j ==> 0<k ==> int k * i < int k * j"
1.57  apply (induct k)
1.58 @@ -156,7 +156,7 @@
1.59  apply (auto simp add: zmult_zless_mono2_lemma)
1.60  done
1.61
1.62 -text{*The integers form an ordered integral domain*}
1.63 +text\<open>The integers form an ordered integral domain\<close>
1.64  instantiation int :: linordered_idom
1.65  begin
1.66
1.67 @@ -198,7 +198,7 @@
1.68    for z1 z2 w :: int
1.69
1.70
1.71 -subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
1.72 +subsection \<open>Embedding of the Integers into any @{text ring_1}: @{text of_int}\<close>
1.73
1.74  context ring_1
1.75  begin
1.76 @@ -225,7 +225,7 @@
1.77  lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
1.78    by (transfer fixing: times) (clarsimp simp add: algebra_simps of_nat_mult)
1.79
1.80 -text{*Collapse nested embeddings*}
1.81 +text\<open>Collapse nested embeddings\<close>
1.82  lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
1.83  by (induct n) auto
1.84
1.85 @@ -249,7 +249,7 @@
1.86    by transfer (clarsimp simp add: algebra_simps
1.88
1.89 -text{*Special cases where either operand is zero*}
1.90 +text\<open>Special cases where either operand is zero\<close>
1.91  lemma of_int_eq_0_iff [simp]:
1.92    "of_int z = 0 \<longleftrightarrow> z = 0"
1.93    using of_int_eq_iff [of z 0] by simp
1.94 @@ -263,7 +263,7 @@
1.95  context linordered_idom
1.96  begin
1.97
1.98 -text{*Every @{text linordered_idom} has characteristic zero.*}
1.99 +text\<open>Every @{text linordered_idom} has characteristic zero.\<close>
1.100  subclass ring_char_0 ..
1.101
1.102  lemma of_int_le_iff [simp]:
1.103 @@ -316,7 +316,7 @@
1.104    apply simp
1.105    done
1.106
1.107 -subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
1.108 +subsection \<open>Magnitude of an Integer, as a Natural Number: @{text nat}\<close>
1.109
1.110  lift_definition nat :: "int \<Rightarrow> nat" is "\<lambda>(x, y). x - y"
1.111    by auto
1.112 @@ -336,7 +336,7 @@
1.113  lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
1.114    by transfer (clarsimp, arith)
1.115
1.116 -text{*An alternative condition is @{term "0 \<le> w"} *}
1.117 +text\<open>An alternative condition is @{term "0 \<le> w"}\<close>
1.118  corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
1.119  by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
1.120
1.121 @@ -432,11 +432,11 @@
1.122    by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
1.123
1.124
1.125 -text {* For termination proofs: *}
1.126 +text \<open>For termination proofs:\<close>
1.127  lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
1.128
1.129
1.130 -subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
1.131 +subsection\<open>Lemmas about the Function @{term of_nat} and Orderings\<close>
1.132
1.133  lemma negative_zless_0: "- (int (Suc n)) < (0 \<Colon> int)"
1.134  by (simp add: order_less_le del: of_nat_Suc)
1.135 @@ -479,10 +479,10 @@
1.136  lemma int_Suc0_eq_1: "int (Suc 0) = 1"
1.137  by simp
1.138
1.139 -text{*This version is proved for all ordered rings, not just integers!
1.140 +text\<open>This version is proved for all ordered rings, not just integers!
1.141        It is proved here because attribute @{text arith_split} is not available
1.142        in theory @{text Rings}.
1.143 -      But is it really better than just rewriting with @{text abs_if}?*}
1.144 +      But is it really better than just rewriting with @{text abs_if}?\<close>
1.145  lemma abs_split [arith_split, no_atp]:
1.146       "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
1.147  by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
1.148 @@ -493,19 +493,19 @@
1.149  apply (rule_tac x="b - Suc a" in exI, arith)
1.150  done
1.151
1.152 -subsection {* Cases and induction *}
1.153 +subsection \<open>Cases and induction\<close>
1.154
1.155 -text{*Now we replace the case analysis rule by a more conventional one:
1.156 -whether an integer is negative or not.*}
1.157 +text\<open>Now we replace the case analysis rule by a more conventional one:
1.158 +whether an integer is negative or not.\<close>
1.159
1.160 -text{*This version is symmetric in the two subgoals.*}
1.161 +text\<open>This version is symmetric in the two subgoals.\<close>
1.162  theorem int_cases2 [case_names nonneg nonpos, cases type: int]:
1.163    "\<lbrakk>!! n. z = int n \<Longrightarrow> P;  !! n. z = - (int n) \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
1.164  apply (cases "z < 0")
1.165  apply (auto simp add: linorder_not_less dest!: negD nat_0_le [THEN sym])
1.166  done
1.167
1.168 -text{*This is the default, with a negative case.*}
1.169 +text\<open>This is the default, with a negative case.\<close>
1.170  theorem int_cases [case_names nonneg neg, cases type: int]:
1.171    "[|!! n. z = int n ==> P;  !! n. z = - (int (Suc n)) ==> P |] ==> P"
1.172  apply (cases "z < 0")
1.173 @@ -524,14 +524,14 @@
1.174    using assms by (rule nonneg_eq_int)
1.175
1.176  lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
1.177 -  -- {* Unfold all @{text let}s involving constants *}
1.178 -  by (fact Let_numeral) -- {* FIXME drop *}
1.179 +  -- \<open>Unfold all @{text let}s involving constants\<close>
1.180 +  by (fact Let_numeral) -- \<open>FIXME drop\<close>
1.181
1.182  lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
1.183 -  -- {* Unfold all @{text let}s involving constants *}
1.184 -  by (fact Let_neg_numeral) -- {* FIXME drop *}
1.185 +  -- \<open>Unfold all @{text let}s involving constants\<close>
1.186 +  by (fact Let_neg_numeral) -- \<open>FIXME drop\<close>
1.187
1.188 -text {* Unfold @{text min} and @{text max} on numerals. *}
1.189 +text \<open>Unfold @{text min} and @{text max} on numerals.\<close>
1.190
1.191  lemmas max_number_of [simp] =
1.192    max_def [of "numeral u" "numeral v"]
1.193 @@ -546,9 +546,9 @@
1.194    min_def [of "- numeral u" "- numeral v"] for u v
1.195
1.196
1.197 -subsubsection {* Binary comparisons *}
1.198 +subsubsection \<open>Binary comparisons\<close>
1.199
1.200 -text {* Preliminaries *}
1.201 +text \<open>Preliminaries\<close>
1.202
1.203  lemma le_imp_0_less:
1.204    assumes le: "0 \<le> z"
1.205 @@ -572,7 +572,7 @@
1.207  qed
1.208
1.209 -subsubsection {* Comparisons, for Ordered Rings *}
1.210 +subsubsection \<open>Comparisons, for Ordered Rings\<close>
1.211
1.212  lemmas double_eq_0_iff = double_zero
1.213
1.214 @@ -599,7 +599,7 @@
1.215  qed
1.216
1.217
1.218 -subsection {* The Set of Integers *}
1.219 +subsection \<open>The Set of Integers\<close>
1.220
1.221  context ring_1
1.222  begin
1.223 @@ -654,7 +654,7 @@
1.224    obtains (of_int) z where "q = of_int z"
1.225    unfolding Ints_def
1.226  proof -
1.227 -  from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def .
1.228 +  from \<open>q \<in> \<int>\<close> have "q \<in> range of_int" unfolding Ints_def .
1.229    then obtain z where "q = of_int z" ..
1.230    then show thesis ..
1.231  qed
1.232 @@ -665,7 +665,7 @@
1.233
1.234  end
1.235
1.236 -text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
1.237 +text \<open>The premise involving @{term Ints} prevents @{term "a = 1/2"}.\<close>
1.238
1.239  lemma Ints_double_eq_0_iff:
1.240    assumes in_Ints: "a \<in> Ints"
1.241 @@ -718,7 +718,7 @@
1.242  qed
1.243
1.244
1.245 -subsection {* @{term setsum} and @{term setprod} *}
1.246 +subsection \<open>@{term setsum} and @{term setprod}\<close>
1.247
1.248  lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
1.249    apply (cases "finite A")
1.250 @@ -744,27 +744,27 @@
1.251  lemmas int_setprod = of_nat_setprod [where 'a=int]
1.252
1.253
1.254 -text {* Legacy theorems *}
1.255 +text \<open>Legacy theorems\<close>
1.256
1.257  lemmas zle_int = of_nat_le_iff [where 'a=int]
1.258  lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
1.259  lemmas numeral_1_eq_1 = numeral_One
1.260
1.261 -subsection {* Setting up simplification procedures *}
1.262 +subsection \<open>Setting up simplification procedures\<close>
1.263
1.264  lemmas of_int_simps =
1.266
1.267  ML_file "Tools/int_arith.ML"
1.268 -declaration {* K Int_Arith.setup *}
1.269 +declaration \<open>K Int_Arith.setup\<close>
1.270
1.271  simproc_setup fast_arith ("(m::'a::linordered_idom) < n" |
1.272    "(m::'a::linordered_idom) <= n" |
1.273    "(m::'a::linordered_idom) = n") =
1.274 -  {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (Thm.term_of ct) *}
1.275 +  \<open>fn _ => fn ss => fn ct => Lin_Arith.simproc ss (Thm.term_of ct)\<close>
1.276
1.277
1.278 -subsection{*More Inequality Reasoning*}
1.279 +subsection\<open>More Inequality Reasoning\<close>
1.280
1.281  lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
1.282  by arith
1.283 @@ -782,15 +782,15 @@
1.284  by arith
1.285
1.286
1.287 -subsection{*The functions @{term nat} and @{term int}*}
1.288 +subsection\<open>The functions @{term nat} and @{term int}\<close>
1.289
1.290 -text{*Simplify the term @{term "w + - z"}*}
1.291 +text\<open>Simplify the term @{term "w + - z"}\<close>
1.292
1.293  lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
1.294    using zless_nat_conj [of 1 z] by auto
1.295
1.296 -text{*This simplifies expressions of the form @{term "int n = z"} where
1.297 -      z is an integer literal.*}
1.298 +text\<open>This simplifies expressions of the form @{term "int n = z"} where
1.299 +      z is an integer literal.\<close>
1.300  lemmas int_eq_iff_numeral [simp] = int_eq_iff [of _ "numeral v"] for v
1.301
1.302  lemma split_nat [arith_split]:
1.303 @@ -895,7 +895,7 @@
1.304
1.305  subsection "Induction principles for int"
1.306
1.307 -text{*Well-founded segments of the integers*}
1.308 +text\<open>Well-founded segments of the integers\<close>
1.309
1.310  definition
1.311    int_ge_less_than  ::  "int => (int * int) set"
1.312 @@ -910,8 +910,8 @@
1.313      by (rule wf_subset [OF wf_measure])
1.314  qed
1.315
1.316 -text{*This variant looks odd, but is typical of the relations suggested
1.317 -by RankFinder.*}
1.318 +text\<open>This variant looks odd, but is typical of the relations suggested
1.319 +by RankFinder.\<close>
1.320
1.321  definition
1.322    int_ge_less_than2 ::  "int => (int * int) set"
1.323 @@ -1021,7 +1021,7 @@
1.324    qed
1.325  qed
1.326
1.327 -subsection{*Intermediate value theorems*}
1.328 +subsection\<open>Intermediate value theorems\<close>
1.329
1.330  lemma int_val_lemma:
1.331       "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
1.332 @@ -1053,7 +1053,7 @@
1.333  done
1.334
1.335
1.336 -subsection{*Products and 1, by T. M. Rasmussen*}
1.337 +subsection\<open>Products and 1, by T. M. Rasmussen\<close>
1.338
1.339  lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
1.340  by arith
1.341 @@ -1110,18 +1110,18 @@
1.342  qed
1.343
1.344
1.345 -subsection {* Further theorems on numerals *}
1.346 +subsection \<open>Further theorems on numerals\<close>
1.347
1.348 -subsubsection{*Special Simplification for Constants*}
1.349 +subsubsection\<open>Special Simplification for Constants\<close>
1.350
1.351 -text{*These distributive laws move literals inside sums and differences.*}
1.352 +text\<open>These distributive laws move literals inside sums and differences.\<close>
1.353
1.354  lemmas distrib_right_numeral [simp] = distrib_right [of _ _ "numeral v"] for v
1.355  lemmas distrib_left_numeral [simp] = distrib_left [of "numeral v"] for v
1.356  lemmas left_diff_distrib_numeral [simp] = left_diff_distrib [of _ _ "numeral v"] for v
1.357  lemmas right_diff_distrib_numeral [simp] = right_diff_distrib [of "numeral v"] for v
1.358
1.359 -text{*These are actually for fields, like real: but where else to put them?*}
1.360 +text\<open>These are actually for fields, like real: but where else to put them?\<close>
1.361
1.362  lemmas zero_less_divide_iff_numeral [simp, no_atp] = zero_less_divide_iff [of "numeral w"] for w
1.363  lemmas divide_less_0_iff_numeral [simp, no_atp] = divide_less_0_iff [of "numeral w"] for w
1.364 @@ -1129,8 +1129,8 @@
1.365  lemmas divide_le_0_iff_numeral [simp, no_atp] = divide_le_0_iff [of "numeral w"] for w
1.366
1.367
1.368 -text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
1.369 -  strange, but then other simprocs simplify the quotient.*}
1.370 +text \<open>Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
1.371 +  strange, but then other simprocs simplify the quotient.\<close>
1.372
1.373  lemmas inverse_eq_divide_numeral [simp] =
1.374    inverse_eq_divide [of "numeral w"] for w
1.375 @@ -1138,8 +1138,8 @@
1.376  lemmas inverse_eq_divide_neg_numeral [simp] =
1.377    inverse_eq_divide [of "- numeral w"] for w
1.378
1.379 -text {*These laws simplify inequalities, moving unary minus from a term
1.380 -into the literal.*}
1.381 +text \<open>These laws simplify inequalities, moving unary minus from a term
1.382 +into the literal.\<close>
1.383
1.384  lemmas equation_minus_iff_numeral [no_atp] =
1.385    equation_minus_iff [of "numeral v"] for v
1.386 @@ -1159,10 +1159,10 @@
1.387  lemmas minus_less_iff_numeral [no_atp] =
1.388    minus_less_iff [of _ "numeral v"] for v
1.389
1.390 --- {* FIXME maybe simproc *}
1.391 +-- \<open>FIXME maybe simproc\<close>
1.392
1.393
1.394 -text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
1.395 +text \<open>Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"})\<close>
1.396
1.397  lemmas mult_less_cancel_left_numeral [simp, no_atp] = mult_less_cancel_left [of "numeral v"] for v
1.398  lemmas mult_less_cancel_right_numeral [simp, no_atp] = mult_less_cancel_right [of _ "numeral v"] for v
1.399 @@ -1170,7 +1170,7 @@
1.400  lemmas mult_le_cancel_right_numeral [simp, no_atp] = mult_le_cancel_right [of _ "numeral v"] for v
1.401
1.402
1.403 -text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
1.404 +text \<open>Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="})\<close>
1.405
1.406  lemmas le_divide_eq_numeral1 [simp] =
1.407    pos_le_divide_eq [of "numeral w", OF zero_less_numeral]
1.408 @@ -1197,9 +1197,9 @@
1.409    divide_eq_eq [of _ "- numeral w"] for w
1.410
1.411
1.412 -subsubsection{*Optional Simplification Rules Involving Constants*}
1.413 +subsubsection\<open>Optional Simplification Rules Involving Constants\<close>
1.414
1.415 -text{*Simplify quotients that are compared with a literal constant.*}
1.416 +text\<open>Simplify quotients that are compared with a literal constant.\<close>
1.417
1.418  lemmas le_divide_eq_numeral =
1.419    le_divide_eq [of "numeral w"]
1.420 @@ -1226,14 +1226,14 @@
1.421    divide_eq_eq [of _ _ "- numeral w"] for w
1.422
1.423
1.424 -text{*Not good as automatic simprules because they cause case splits.*}
1.425 +text\<open>Not good as automatic simprules because they cause case splits.\<close>
1.426  lemmas divide_const_simps =
1.427    le_divide_eq_numeral divide_le_eq_numeral less_divide_eq_numeral
1.428    divide_less_eq_numeral eq_divide_eq_numeral divide_eq_eq_numeral
1.429    le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
1.430
1.431
1.432 -subsection {* The divides relation *}
1.433 +subsection \<open>The divides relation\<close>
1.434
1.435  lemma zdvd_antisym_nonneg:
1.436      "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)"
1.437 @@ -1247,11 +1247,11 @@
1.438    assume "a = 0" with assms show ?thesis by simp
1.439  next
1.440    assume "a \<noteq> 0"
1.441 -  from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
1.442 -  from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
1.443 +  from \<open>a dvd b\<close> obtain k where k:"b = a*k" unfolding dvd_def by blast
1.444 +  from \<open>b dvd a\<close> obtain k' where k':"a = b*k'" unfolding dvd_def by blast
1.445    from k k' have "a = a*k*k'" by simp
1.446    with mult_cancel_left1[where c="a" and b="k*k'"]
1.447 -  have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult.assoc)
1.448 +  have kk':"k*k' = 1" using \<open>a\<noteq>0\<close> by (simp add: mult.assoc)
1.449    hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
1.450    thus ?thesis using k k' by auto
1.451  qed
1.452 @@ -1267,11 +1267,11 @@
1.453    assumes "i \<noteq> 0" and "d dvd i"
1.454    shows "\<bar>d\<bar> \<le> \<bar>i\<bar>"
1.455  proof -
1.456 -  from `d dvd i` obtain k where "i = d * k" ..
1.457 -  with `i \<noteq> 0` have "k \<noteq> 0" by auto
1.458 +  from \<open>d dvd i\<close> obtain k where "i = d * k" ..
1.459 +  with \<open>i \<noteq> 0\<close> have "k \<noteq> 0" by auto
1.460    then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto
1.461    then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono)
1.462 -  with `i = d * k` show ?thesis by (simp add: abs_mult)
1.463 +  with \<open>i = d * k\<close> show ?thesis by (simp add: abs_mult)
1.464  qed
1.465
1.466  lemma zdvd_not_zless:
1.467 @@ -1281,10 +1281,10 @@
1.468  proof
1.469    from assms have "0 < n" by auto
1.470    assume "n dvd m" then obtain k where k: "m = n * k" ..
1.471 -  with `0 < m` have "0 < n * k" by auto
1.472 -  with `0 < n` have "0 < k" by (simp add: zero_less_mult_iff)
1.473 -  with k `0 < n` `m < n` have "n * k < n * 1" by simp
1.474 -  with `0 < n` `0 < k` show False unfolding mult_less_cancel_left by auto
1.475 +  with \<open>0 < m\<close> have "0 < n * k" by auto
1.476 +  with \<open>0 < n\<close> have "0 < k" by (simp add: zero_less_mult_iff)
1.477 +  with k \<open>0 < n\<close> \<open>m < n\<close> have "n * k < n * 1" by simp
1.478 +  with \<open>0 < n\<close> \<open>0 < k\<close> show False unfolding mult_less_cancel_left by auto
1.479  qed
1.480
1.481  lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
1.482 @@ -1381,17 +1381,17 @@
1.483      assume "a dvd (x + t)"
1.484      then obtain l where "x + t = a * l" by (rule dvdE)
1.485      then have "x = a * l - t" by simp
1.486 -    with `d = a * k` show "a dvd x + c * d + t" by simp
1.487 +    with \<open>d = a * k\<close> show "a dvd x + c * d + t" by simp
1.488    next
1.489      assume "a dvd x + c * d + t"
1.490      then obtain l where "x + c * d + t = a * l" by (rule dvdE)
1.491      then have "x = a * l - c * d - t" by simp
1.492 -    with `d = a * k` show "a dvd (x + t)" by simp
1.493 +    with \<open>d = a * k\<close> show "a dvd (x + t)" by simp
1.494    qed
1.495  qed
1.496
1.497
1.498 -subsection {* Finiteness of intervals *}
1.499 +subsection \<open>Finiteness of intervals\<close>
1.500
1.501  lemma finite_interval_int1 [iff]: "finite {i :: int. a <= i & i <= b}"
1.502  proof (cases "a <= b")
1.503 @@ -1421,9 +1421,9 @@
1.504  by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
1.505
1.506
1.507 -subsection {* Configuration of the code generator *}
1.508 +subsection \<open>Configuration of the code generator\<close>
1.509
1.510 -text {* Constructors *}
1.511 +text \<open>Constructors\<close>
1.512
1.513  definition Pos :: "num \<Rightarrow> int" where
1.514    [simp, code_abbrev]: "Pos = numeral"
1.515 @@ -1434,7 +1434,7 @@
1.516  code_datatype "0::int" Pos Neg
1.517
1.518
1.519 -text {* Auxiliary operations *}
1.520 +text \<open>Auxiliary operations\<close>
1.521
1.522  definition dup :: "int \<Rightarrow> int" where
1.523    [simp]: "dup k = k + k"
1.524 @@ -1465,7 +1465,7 @@
1.526    done
1.527
1.528 -text {* Implementations *}
1.529 +text \<open>Implementations\<close>
1.530
1.531  lemma one_int_code [code, code_unfold]:
1.532    "1 = Pos Num.One"
1.533 @@ -1567,7 +1567,7 @@
1.534    by simp_all
1.535
1.536
1.537 -text {* Serializer setup *}
1.538 +text \<open>Serializer setup\<close>
1.539
1.540  code_identifier
1.541    code_module Int \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
1.542 @@ -1577,7 +1577,7 @@
1.543  hide_const (open) Pos Neg sub dup
1.544
1.545
1.546 -subsection {* Legacy theorems *}
1.547 +subsection \<open>Legacy theorems\<close>
1.548
1.549  lemmas inj_int = inj_of_nat [where 'a=int]
1.551 @@ -1609,12 +1609,12 @@
1.552
1.553  lemmas zpower_int = int_power [symmetric]
1.554
1.555 -text {* De-register @{text "int"} as a quotient type: *}
1.556 +text \<open>De-register @{text "int"} as a quotient type:\<close>
1.557
1.558  lifting_update int.lifting
1.559  lifting_forget int.lifting
1.560
1.561 -text{*Also the class for fields with characteristic zero.*}
1.562 +text\<open>Also the class for fields with characteristic zero.\<close>
1.563  class field_char_0 = field + ring_char_0
1.564  subclass (in linordered_field) field_char_0 ..
1.565
```