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.28  by (rule trans [OF mod_add_left_eq mod_add_right_eq])
    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])