diff -r f6b0d827240e -r bdc1e2f0a86a src/HOL/Divides.thy --- a/src/HOL/Divides.thy Tue Sep 01 17:25:36 2015 +0200 +++ b/src/HOL/Divides.thy Tue Sep 01 22:32:58 2015 +0200 @@ -814,8 +814,8 @@ text \ We define @{const divide} and @{const mod} on @{typ nat} by means of a characteristic relation with two input arguments - @{term "m\nat"}, @{term "n\nat"} and two output arguments - @{term "q\nat"}(uotient) and @{term "r\nat"}(emainder). + @{term "m::nat"}, @{term "n::nat"} and two output arguments + @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder). \ definition divmod_nat_rel :: "nat \ nat \ nat \ nat \ bool" where @@ -835,7 +835,7 @@ have "\q r. m = q * n + r \ r < n" proof (induct m) case 0 with \n \ 0\ - have "(0\nat) = 0 * n + 0 \ 0 < n" by simp + have "(0::nat) = 0 * n + 0 \ 0 < n" by simp then show ?case by blast next case (Suc m) then obtain q' r' @@ -868,7 +868,7 @@ (simp add: divmod_nat_rel_def) next case False - have aux: "\q r q' r'. q' * n + r' = q * n + r \ r < n \ q' \ (q\nat)" + have aux: "\q r q' r'. q' * n + r' = q * n + r \ r < n \ q' \ (q::nat)" apply (rule leI) apply (subst less_iff_Suc_add) apply (auto simp add: add_mult_distrib) @@ -1115,10 +1115,10 @@ then show "m div n * n + m mod n \ m" by auto qed -lemma mod_geq: "\ m < (n\nat) \ m mod n = (m - n) mod n" +lemma mod_geq: "\ m < (n::nat) \ m mod n = (m - n) mod n" by (simp add: le_mod_geq linorder_not_less) -lemma mod_if: "m mod (n\nat) = (if m < n then m else (m - n) mod n)" +lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)" by (simp add: le_mod_geq) lemma mod_1 [simp]: "m mod Suc 0 = 0" @@ -1313,7 +1313,7 @@ lemma split_div_lemma: assumes "0 < n" - shows "n * q \ m \ m < n * Suc q \ q = ((m\nat) div n)" (is "?lhs \ ?rhs") + shows "n * q \ m \ m < n * Suc q \ q = ((m::nat) div n)" (is "?lhs \ ?rhs") proof assume ?rhs with mult_div_cancel have nq: "n * q = m - (m mod n)" by simp @@ -1486,7 +1486,7 @@ lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)" by (simp add: mult_2 [symmetric]) -lemma mod2_gr_0 [simp]: "0 < (m\nat) mod 2 \ m mod 2 = 1" +lemma mod2_gr_0 [simp]: "0 < (m::nat) mod 2 \ m mod 2 = 1" proof - { fix n :: nat have "(n::nat) < 2 \ n = 0 \ n = 1" by (cases n) simp_all } moreover have "m mod 2 < 2" by simp @@ -1999,7 +1999,7 @@ lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1] lemma zmod_zdiv_equality' [nitpick_unfold]: - "(m\int) mod n = m - (m div n) * n" + "(m::int) mod n = m - (m div n) * n" using mod_div_equality [of m n] by arith