src/HOL/Divides.thy
changeset 45607 16b4f5774621
parent 45530 0c4853bb77bf
child 46026 83caa4f4bd56
     1.1 --- a/src/HOL/Divides.thy	Sun Nov 20 21:07:06 2011 +0100
     1.2 +++ b/src/HOL/Divides.thy	Sun Nov 20 21:07:10 2011 +0100
     1.3 @@ -1142,13 +1142,8 @@
     1.4  lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
     1.5  by (simp add: Suc3_eq_add_3)
     1.6  
     1.7 -lemmas Suc_div_eq_add3_div_number_of =
     1.8 -    Suc_div_eq_add3_div [of _ "number_of v", standard]
     1.9 -declare Suc_div_eq_add3_div_number_of [simp]
    1.10 -
    1.11 -lemmas Suc_mod_eq_add3_mod_number_of =
    1.12 -    Suc_mod_eq_add3_mod [of _ "number_of v", standard]
    1.13 -declare Suc_mod_eq_add3_mod_number_of [simp]
    1.14 +lemmas Suc_div_eq_add3_div_number_of [simp] = Suc_div_eq_add3_div [of _ "number_of v"] for v
    1.15 +lemmas Suc_mod_eq_add3_mod_number_of [simp] = Suc_mod_eq_add3_mod [of _ "number_of v"] for v
    1.16  
    1.17  
    1.18  lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" 
    1.19 @@ -1156,7 +1151,7 @@
    1.20  apply (simp_all add: mod_Suc)
    1.21  done
    1.22  
    1.23 -declare Suc_times_mod_eq [of "number_of w", standard, simp]
    1.24 +declare Suc_times_mod_eq [of "number_of w", simp] for w
    1.25  
    1.26  lemma [simp]: "n div k \<le> (Suc n) div k"
    1.27  by (simp add: div_le_mono) 
    1.28 @@ -1450,17 +1445,16 @@
    1.29  apply (auto simp add: divmod_int_rel_def mod_int_def)
    1.30  done
    1.31  
    1.32 -lemmas pos_mod_sign  [simp] = pos_mod_conj [THEN conjunct1, standard]
    1.33 -   and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2, standard]
    1.34 +lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
    1.35 +   and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
    1.36  
    1.37  lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
    1.38  apply (cut_tac a = a and b = b in divmod_int_correct)
    1.39  apply (auto simp add: divmod_int_rel_def div_int_def mod_int_def)
    1.40  done
    1.41  
    1.42 -lemmas neg_mod_sign  [simp] = neg_mod_conj [THEN conjunct1, standard]
    1.43 -   and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2, standard]
    1.44 -
    1.45 +lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
    1.46 +   and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
    1.47  
    1.48  
    1.49  subsubsection{*General Properties of div and mod*}
    1.50 @@ -1728,11 +1722,8 @@
    1.51  simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
    1.52    {* K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq}) *}
    1.53  
    1.54 -lemmas posDivAlg_eqn_number_of [simp] =
    1.55 -    posDivAlg_eqn [of "number_of v" "number_of w", standard]
    1.56 -
    1.57 -lemmas negDivAlg_eqn_number_of [simp] =
    1.58 -    negDivAlg_eqn [of "number_of v" "number_of w", standard]
    1.59 +lemmas posDivAlg_eqn_number_of [simp] = posDivAlg_eqn [of "number_of v" "number_of w"] for v w
    1.60 +lemmas negDivAlg_eqn_number_of [simp] = negDivAlg_eqn [of "number_of v" "number_of w"] for v w
    1.61  
    1.62  
    1.63  text{*Special-case simplification *}
    1.64 @@ -1749,25 +1740,12 @@
    1.65  (** The last remaining special cases for constant arithmetic:
    1.66      1 div z and 1 mod z **)
    1.67  
    1.68 -lemmas div_pos_pos_1_number_of [simp] =
    1.69 -    div_pos_pos [OF zero_less_one, of "number_of w", standard]
    1.70 -
    1.71 -lemmas div_pos_neg_1_number_of [simp] =
    1.72 -    div_pos_neg [OF zero_less_one, of "number_of w", standard]
    1.73 -
    1.74 -lemmas mod_pos_pos_1_number_of [simp] =
    1.75 -    mod_pos_pos [OF zero_less_one, of "number_of w", standard]
    1.76 -
    1.77 -lemmas mod_pos_neg_1_number_of [simp] =
    1.78 -    mod_pos_neg [OF zero_less_one, of "number_of w", standard]
    1.79 -
    1.80 -
    1.81 -lemmas posDivAlg_eqn_1_number_of [simp] =
    1.82 -    posDivAlg_eqn [of concl: 1 "number_of w", standard]
    1.83 -
    1.84 -lemmas negDivAlg_eqn_1_number_of [simp] =
    1.85 -    negDivAlg_eqn [of concl: 1 "number_of w", standard]
    1.86 -
    1.87 +lemmas div_pos_pos_1_number_of [simp] = div_pos_pos [OF zero_less_one, of "number_of w"] for w
    1.88 +lemmas div_pos_neg_1_number_of [simp] = div_pos_neg [OF zero_less_one, of "number_of w"] for w
    1.89 +lemmas mod_pos_pos_1_number_of [simp] = mod_pos_pos [OF zero_less_one, of "number_of w"] for w
    1.90 +lemmas mod_pos_neg_1_number_of [simp] = mod_pos_neg [OF zero_less_one, of "number_of w"] for w
    1.91 +lemmas posDivAlg_eqn_1_number_of [simp] = posDivAlg_eqn [of concl: 1 "number_of w"] for w
    1.92 +lemmas negDivAlg_eqn_1_number_of [simp] = negDivAlg_eqn [of concl: 1 "number_of w"] for w
    1.93  
    1.94  
    1.95  subsubsection{*Monotonicity in the First Argument (Dividend)*}
    1.96 @@ -2069,8 +2047,8 @@
    1.97  text {* Enable (lin)arith to deal with @{const div} and @{const mod}
    1.98    when these are applied to some constant that is of the form
    1.99    @{term "number_of k"}: *}
   1.100 -declare split_zdiv [of _ _ "number_of k", standard, arith_split]
   1.101 -declare split_zmod [of _ _ "number_of k", standard, arith_split]
   1.102 +declare split_zdiv [of _ _ "number_of k", arith_split] for k
   1.103 +declare split_zmod [of _ _ "number_of k", arith_split] for k
   1.104  
   1.105  
   1.106  subsubsection{*Speeding up the Division Algorithm with Shifting*}
   1.107 @@ -2257,7 +2235,7 @@
   1.108  subsubsection {* The Divides Relation *}
   1.109  
   1.110  lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
   1.111 -  dvd_eq_mod_eq_0 [of "number_of x::int" "number_of y::int", standard]
   1.112 +  dvd_eq_mod_eq_0 [of "number_of x" "number_of y"] for x y :: int
   1.113  
   1.114  lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
   1.115    by (rule dvd_mod) (* TODO: remove *)
   1.116 @@ -2456,10 +2434,8 @@
   1.117           else nat (1 mod number_of v'))"
   1.118  by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
   1.119  
   1.120 -lemmas dvd_eq_mod_eq_0_number_of =
   1.121 -  dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
   1.122 -
   1.123 -declare dvd_eq_mod_eq_0_number_of [simp]
   1.124 +lemmas dvd_eq_mod_eq_0_number_of [simp] =
   1.125 +  dvd_eq_mod_eq_0 [of "number_of x" "number_of y"] for x y
   1.126  
   1.127  
   1.128  subsubsection {* Nitpick *}