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.44  instance int :: ordered_cancel_ab_semigroup_add
    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.87      of_nat_add [symmetric] simp del: of_nat_add)
    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.206      add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
   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.265    of_int_0 of_int_1 of_int_add of_int_mult
   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.525    apply (simp_all only: minus_add add.assoc left_minus)
   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.550  lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
   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