src/HOL/Divides.thy
 changeset 61799 4cf66f21b764 parent 61649 268d88ec9087 child 61944 5d06ecfdb472
```     1.1 --- a/src/HOL/Divides.thy	Mon Dec 07 10:23:50 2015 +0100
1.2 +++ b/src/HOL/Divides.thy	Mon Dec 07 10:38:04 2015 +0100
1.3 @@ -220,7 +220,7 @@
1.4
1.5  text \<open>Addition respects modular equivalence.\<close>
1.6
1.7 -lemma mod_add_left_eq: -- \<open>FIXME reorient\<close>
1.8 +lemma mod_add_left_eq: \<comment> \<open>FIXME reorient\<close>
1.9    "(a + b) mod c = (a mod c + b) mod c"
1.10  proof -
1.11    have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
1.12 @@ -232,7 +232,7 @@
1.13    finally show ?thesis .
1.14  qed
1.15
1.16 -lemma mod_add_right_eq: -- \<open>FIXME reorient\<close>
1.17 +lemma mod_add_right_eq: \<comment> \<open>FIXME reorient\<close>
1.18    "(a + b) mod c = (a + b mod c) mod c"
1.19  proof -
1.20    have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
1.21 @@ -244,7 +244,7 @@
1.22    finally show ?thesis .
1.23  qed
1.24
1.25 -lemma mod_add_eq: -- \<open>FIXME reorient\<close>
1.26 +lemma mod_add_eq: \<comment> \<open>FIXME reorient\<close>
1.27    "(a + b) mod c = (a mod c + b mod c) mod c"
1.29
1.30 @@ -261,7 +261,7 @@
1.31
1.32  text \<open>Multiplication respects modular equivalence.\<close>
1.33
1.34 -lemma mod_mult_left_eq: -- \<open>FIXME reorient\<close>
1.35 +lemma mod_mult_left_eq: \<comment> \<open>FIXME reorient\<close>
1.36    "(a * b) mod c = ((a mod c) * b) mod c"
1.37  proof -
1.38    have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
1.39 @@ -273,7 +273,7 @@
1.40    finally show ?thesis .
1.41  qed
1.42
1.43 -lemma mod_mult_right_eq: -- \<open>FIXME reorient\<close>
1.44 +lemma mod_mult_right_eq: \<comment> \<open>FIXME reorient\<close>
1.45    "(a * b) mod c = (a * (b mod c)) mod c"
1.46  proof -
1.47    have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
1.48 @@ -285,7 +285,7 @@
1.49    finally show ?thesis .
1.50  qed
1.51
1.52 -lemma mod_mult_eq: -- \<open>FIXME reorient\<close>
1.53 +lemma mod_mult_eq: \<comment> \<open>FIXME reorient\<close>
1.54    "(a * b) mod c = ((a mod c) * (b mod c)) mod c"
1.55  by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])
1.56
1.57 @@ -573,7 +573,7 @@
1.58      and divmod_step_def: "divmod_step l qr = (let (q, r) = qr
1.59      in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
1.60      else (2 * q, r))"
1.61 -    -- \<open>These are conceptually definitions but force generated code
1.62 +    \<comment> \<open>These are conceptually definitions but force generated code
1.63      to be monomorphic wrt. particular instances of this class which
1.64      yields a significant speedup.\<close>
1.65
1.66 @@ -733,7 +733,7 @@
1.67    with False show ?thesis by simp
1.68  qed
1.69
1.70 -text \<open>The division rewrite proper -- first, trivial results involving @{text 1}\<close>
1.71 +text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close>
1.72
1.73  lemma divmod_trivial [simp]:
1.74    "divmod Num.One Num.One = (numeral Num.One, 0)"
1.75 @@ -1428,7 +1428,7 @@
1.76      fix k
1.77      show "?A k"
1.78      proof (induct k)
1.79 -      show "?A 0" by simp  -- "by contradiction"
1.80 +      show "?A 0" by simp  \<comment> "by contradiction"
1.81      next
1.82        fix n
1.83        assume ih: "?A n"
1.84 @@ -1638,7 +1638,7 @@
1.85
1.86  subsection \<open>Division on @{typ int}\<close>
1.87
1.88 -definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" -- \<open>definition of quotient and remainder\<close>
1.89 +definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" \<comment> \<open>definition of quotient and remainder\<close>
1.90    where "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
1.91      (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
1.92
1.93 @@ -1860,7 +1860,7 @@
1.94  apply (auto simp add: divmod_int_rel_def)
1.95  done
1.96
1.97 -text\<open>There is no @{text mod_neg_pos_trivial}.\<close>
1.98 +text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
1.99
1.100
1.101  subsubsection \<open>Laws for div and mod with Unary Minus\<close>
1.102 @@ -2170,7 +2170,7 @@
1.103  declare split_zmod [of _ _ "numeral k", arith_split] for k
1.104
1.105
1.106 -subsubsection \<open>Computing @{text "div"} and @{text "mod"} with shifting\<close>
1.107 +subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
1.108
1.109  lemma pos_divmod_int_rel_mult_2:
1.110    assumes "0 \<le> b"
1.111 @@ -2272,8 +2272,8 @@
1.112  lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
1.113  by (drule zdiv_mono1, auto)
1.114
1.115 -text\<open>Now for some equivalences of the form @{text"a div b >=< 0 \<longleftrightarrow> \<dots>"}
1.116 -conditional upon the sign of @{text a} or @{text b}. There are many more.
1.117 +text\<open>Now for some equivalences of the form \<open>a div b >=< 0 \<longleftrightarrow> \<dots>\<close>
1.118 +conditional upon the sign of \<open>a\<close> or \<open>b\<close>. There are many more.
1.119  They should all be simp rules unless that causes too much search.\<close>
1.120
1.121  lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
1.122 @@ -2466,7 +2466,7 @@
1.123    power_mod
1.124    zminus_zmod zdiff_zmod_left zdiff_zmod_right
1.125
1.126 -text \<open>Distributive laws for function @{text nat}.\<close>
1.127 +text \<open>Distributive laws for function \<open>nat\<close>.\<close>
1.128
1.129  lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
1.130  apply (rule linorder_cases [of y 0])
```