src/HOL/Divides.thy

 by (simp add: Suc3_eq_add_3)
 
 lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
 by (simp add: Suc3_eq_add_3)
 
-lemmas Suc_div_eq_add3_div_number_of =
-    Suc_div_eq_add3_div [of _ "number_of v", standard]
-declare Suc_div_eq_add3_div_number_of [simp]
-
-lemmas Suc_mod_eq_add3_mod_number_of =
-    Suc_mod_eq_add3_mod [of _ "number_of v", standard]
-declare Suc_mod_eq_add3_mod_number_of [simp]
+lemmas Suc_div_eq_add3_div_number_of [simp] = Suc_div_eq_add3_div [of _ "number_of v"] for v
+lemmas Suc_mod_eq_add3_mod_number_of [simp] = Suc_mod_eq_add3_mod [of _ "number_of v"] for v
 
 
 lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" 
 apply (induct "m")
 apply (simp_all add: mod_Suc)
 done
 
-declare Suc_times_mod_eq [of "number_of w", standard, simp]
+declare Suc_times_mod_eq [of "number_of w", simp] for w
 
 lemma [simp]: "n div k \<le> (Suc n) div k"
 by (simp add: div_le_mono) 
 
 lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"

 lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
 apply (cut_tac a = a and b = b in divmod_int_correct)
 apply (auto simp add: divmod_int_rel_def mod_int_def)
 done
 
-lemmas pos_mod_sign  [simp] = pos_mod_conj [THEN conjunct1, standard]
-   and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2, standard]
+lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
+   and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
 
 lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
 apply (cut_tac a = a and b = b in divmod_int_correct)
 apply (auto simp add: divmod_int_rel_def div_int_def mod_int_def)
 done
 
-lemmas neg_mod_sign  [simp] = neg_mod_conj [THEN conjunct1, standard]
-   and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2, standard]
-
+lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
+   and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
 
 
 subsubsection{*General Properties of div and mod*}
 
 lemma divmod_int_rel_div_mod: "b \<noteq> 0 ==> divmod_int_rel a b (a div b, a mod b)"

   {* K (divmod_proc @{thm int_div_pos_eq} @{thm int_div_neg_eq}) *}
 
 simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
   {* K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq}) *}
 
-lemmas posDivAlg_eqn_number_of [simp] =
-    posDivAlg_eqn [of "number_of v" "number_of w", standard]
-
-lemmas negDivAlg_eqn_number_of [simp] =
-    negDivAlg_eqn [of "number_of v" "number_of w", standard]
+lemmas posDivAlg_eqn_number_of [simp] = posDivAlg_eqn [of "number_of v" "number_of w"] for v w
+lemmas negDivAlg_eqn_number_of [simp] = negDivAlg_eqn [of "number_of v" "number_of w"] for v w
 
 
 text{*Special-case simplification *}
 
 lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0"

 by (cut_tac a = a and b = "-1" in zmod_zdiv_equality, auto)
 
 (** The last remaining special cases for constant arithmetic:
     1 div z and 1 mod z **)
 
-lemmas div_pos_pos_1_number_of [simp] =
-    div_pos_pos [OF zero_less_one, of "number_of w", standard]
-
-lemmas div_pos_neg_1_number_of [simp] =
-    div_pos_neg [OF zero_less_one, of "number_of w", standard]
-
-lemmas mod_pos_pos_1_number_of [simp] =
-    mod_pos_pos [OF zero_less_one, of "number_of w", standard]
-
-lemmas mod_pos_neg_1_number_of [simp] =
-    mod_pos_neg [OF zero_less_one, of "number_of w", standard]
-
-
-lemmas posDivAlg_eqn_1_number_of [simp] =
-    posDivAlg_eqn [of concl: 1 "number_of w", standard]
-
-lemmas negDivAlg_eqn_1_number_of [simp] =
-    negDivAlg_eqn [of concl: 1 "number_of w", standard]
-
+lemmas div_pos_pos_1_number_of [simp] = div_pos_pos [OF zero_less_one, of "number_of w"] for w
+lemmas div_pos_neg_1_number_of [simp] = div_pos_neg [OF zero_less_one, of "number_of w"] for w
+lemmas mod_pos_pos_1_number_of [simp] = mod_pos_pos [OF zero_less_one, of "number_of w"] for w
+lemmas mod_pos_neg_1_number_of [simp] = mod_pos_neg [OF zero_less_one, of "number_of w"] for w
+lemmas posDivAlg_eqn_1_number_of [simp] = posDivAlg_eqn [of concl: 1 "number_of w"] for w
+lemmas negDivAlg_eqn_1_number_of [simp] = negDivAlg_eqn [of concl: 1 "number_of w"] for w
 
 
 subsubsection{*Monotonicity in the First Argument (Dividend)*}
 
 lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"

 done
 
 text {* Enable (lin)arith to deal with @{const div} and @{const mod}
   when these are applied to some constant that is of the form
   @{term "number_of k"}: *}
-declare split_zdiv [of _ _ "number_of k", standard, arith_split]
-declare split_zmod [of _ _ "number_of k", standard, arith_split]
+declare split_zdiv [of _ _ "number_of k", arith_split] for k
+declare split_zmod [of _ _ "number_of k", arith_split] for k
 
 
 subsubsection{*Speeding up the Division Algorithm with Shifting*}
 
 text{*computing div by shifting *}

 
 
 subsubsection {* The Divides Relation *}
 
 lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
-  dvd_eq_mod_eq_0 [of "number_of x::int" "number_of y::int", standard]
+  dvd_eq_mod_eq_0 [of "number_of x" "number_of y"] for x y :: int
 
 lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
   by (rule dvd_mod) (* TODO: remove *)
 
 lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"

      "Suc 0 mod number_of v' =  
         (if neg (number_of v' :: int) then Suc 0
          else nat (1 mod number_of v'))"
 by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
 
-lemmas dvd_eq_mod_eq_0_number_of =
-  dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
-
-declare dvd_eq_mod_eq_0_number_of [simp]
+lemmas dvd_eq_mod_eq_0_number_of [simp] =
+  dvd_eq_mod_eq_0 [of "number_of x" "number_of y"] for x y
 
 
 subsubsection {* Nitpick *}
 
 lemma zmod_zdiv_equality':