src/HOL/Divides.thy

   then show ?thesis by (simp add: mod_div_equality)
 qed
 
 text \<open>Addition respects modular equivalence.\<close>
 
-lemma mod_add_left_eq: -- \<open>FIXME reorient\<close>
+lemma mod_add_left_eq: \<comment> \<open>FIXME reorient\<close>
   "(a + b) mod c = (a mod c + b) mod c"
 proof -
   have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
     by (simp only: mod_div_equality)
   also have "\<dots> = (a mod c + b + a div c * c) mod c"

   also have "\<dots> = (a mod c + b) mod c"
     by (rule mod_mult_self1)
   finally show ?thesis .
 qed
 
-lemma mod_add_right_eq: -- \<open>FIXME reorient\<close>
+lemma mod_add_right_eq: \<comment> \<open>FIXME reorient\<close>
   "(a + b) mod c = (a + b mod c) mod c"
 proof -
   have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
     by (simp only: mod_div_equality)
   also have "\<dots> = (a + b mod c + b div c * c) mod c"

   also have "\<dots> = (a + b mod c) mod c"
     by (rule mod_mult_self1)
   finally show ?thesis .
 qed
 
-lemma mod_add_eq: -- \<open>FIXME reorient\<close>
+lemma mod_add_eq: \<comment> \<open>FIXME reorient\<close>
   "(a + b) mod c = (a mod c + b mod c) mod c"
 by (rule trans [OF mod_add_left_eq mod_add_right_eq])
 
 lemma mod_add_cong:
   assumes "a mod c = a' mod c"

     by (simp only: mod_add_eq [symmetric])
 qed
 
 text \<open>Multiplication respects modular equivalence.\<close>
 
-lemma mod_mult_left_eq: -- \<open>FIXME reorient\<close>
+lemma mod_mult_left_eq: \<comment> \<open>FIXME reorient\<close>
   "(a * b) mod c = ((a mod c) * b) mod c"
 proof -
   have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
     by (simp only: mod_div_equality)
   also have "\<dots> = (a mod c * b + a div c * b * c) mod c"

   also have "\<dots> = (a mod c * b) mod c"
     by (rule mod_mult_self1)
   finally show ?thesis .
 qed
 
-lemma mod_mult_right_eq: -- \<open>FIXME reorient\<close>
+lemma mod_mult_right_eq: \<comment> \<open>FIXME reorient\<close>
   "(a * b) mod c = (a * (b mod c)) mod c"
 proof -
   have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
     by (simp only: mod_div_equality)
   also have "\<dots> = (a * (b mod c) + a * (b div c) * c) mod c"

   also have "\<dots> = (a * (b mod c)) mod c"
     by (rule mod_mult_self1)
   finally show ?thesis .
 qed
 
-lemma mod_mult_eq: -- \<open>FIXME reorient\<close>
+lemma mod_mult_eq: \<comment> \<open>FIXME reorient\<close>
   "(a * b) mod c = ((a mod c) * (b mod c)) mod c"
 by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])
 
 lemma mod_mult_cong:
   assumes "a mod c = a' mod c"

     and divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
   assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
     and divmod_step_def: "divmod_step l qr = (let (q, r) = qr
     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
     else (2 * q, r))"
-    -- \<open>These are conceptually definitions but force generated code
+    \<comment> \<open>These are conceptually definitions but force generated code
     to be monomorphic wrt. particular instances of this class which
     yields a significant speedup.\<close>
 
 begin
 

   then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
     by (simp add: divmod_def)
   with False show ?thesis by simp
 qed
 
-text \<open>The division rewrite proper -- first, trivial results involving @{text 1}\<close>
+text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close>
 
 lemma divmod_trivial [simp]:
   "divmod Num.One Num.One = (numeral Num.One, 0)"
   "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)"
   "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)"

   have "\<forall>k. 0<k \<longrightarrow> \<not> P (p-k)" (is "\<forall>k. ?A k")
   proof
     fix k
     show "?A k"
     proof (induct k)
-      show "?A 0" by simp  -- "by contradiction"
+      show "?A 0" by simp  \<comment> "by contradiction"
     next
       fix n
       assume ih: "?A n"
       show "?A (Suc n)"
       proof (clarsimp)

   by (simp_all add: snd_divmod)
 
 
 subsection \<open>Division on @{typ int}\<close>
 
-definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" -- \<open>definition of quotient and remainder\<close>
+definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" \<comment> \<open>definition of quotient and remainder\<close>
   where "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
     (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
 
 lemma unique_quotient_lemma:
   "b * q' + r' \<le> b * q + r \<Longrightarrow> 0 \<le> r' \<Longrightarrow> r' < b \<Longrightarrow> r < b \<Longrightarrow> q' \<le> (q::int)"

 lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
 apply (rule_tac q = "-1" in mod_int_unique)
 apply (auto simp add: divmod_int_rel_def)
 done
 
-text\<open>There is no @{text mod_neg_pos_trivial}.\<close>
+text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
 
 
 subsubsection \<open>Laws for div and mod with Unary Minus\<close>
 
 lemma zminus1_lemma:

   @{term "numeral k"}:\<close>
 declare split_zdiv [of _ _ "numeral k", arith_split] for k
 declare split_zmod [of _ _ "numeral k", arith_split] for k
 
 
-subsubsection \<open>Computing @{text "div"} and @{text "mod"} with shifting\<close>
+subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
 
 lemma pos_divmod_int_rel_mult_2:
   assumes "0 \<le> b"
   assumes "divmod_int_rel a b (q, r)"
   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"

 by (drule zdiv_mono1_neg, auto)
 
 lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
 by (drule zdiv_mono1, auto)
 
-text\<open>Now for some equivalences of the form @{text"a div b >=< 0 \<longleftrightarrow> \<dots>"}
-conditional upon the sign of @{text a} or @{text b}. There are many more.
+text\<open>Now for some equivalences of the form \<open>a div b >=< 0 \<longleftrightarrow> \<dots>\<close>
+conditional upon the sign of \<open>a\<close> or \<open>b\<close>. There are many more.
 They should all be simp rules unless that causes too much search.\<close>
 
 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
 apply auto
 apply (drule_tac [2] zdiv_mono1)

   mod_mult_right_eq[symmetric]
   mod_mult_left_eq [symmetric]
   power_mod
   zminus_zmod zdiff_zmod_left zdiff_zmod_right
 
-text \<open>Distributive laws for function @{text nat}.\<close>
+text \<open>Distributive laws for function \<open>nat\<close>.\<close>
 
 lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
 apply (rule linorder_cases [of y 0])
 apply (simp add: div_nonneg_neg_le0)
 apply simp