src/HOL/Divides.thy
 changeset 61076 bdc1e2f0a86a parent 60930 dd8ab7252ba2 child 61201 94efa2688ff6
```     1.1 --- a/src/HOL/Divides.thy	Tue Sep 01 17:25:36 2015 +0200
1.2 +++ b/src/HOL/Divides.thy	Tue Sep 01 22:32:58 2015 +0200
1.3 @@ -814,8 +814,8 @@
1.4  text \<open>
1.5    We define @{const divide} and @{const mod} on @{typ nat} by means
1.6    of a characteristic relation with two input arguments
1.7 -  @{term "m\<Colon>nat"}, @{term "n\<Colon>nat"} and two output arguments
1.8 -  @{term "q\<Colon>nat"}(uotient) and @{term "r\<Colon>nat"}(emainder).
1.9 +  @{term "m::nat"}, @{term "n::nat"} and two output arguments
1.10 +  @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder).
1.11  \<close>
1.12
1.13  definition divmod_nat_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
1.14 @@ -835,7 +835,7 @@
1.15    have "\<exists>q r. m = q * n + r \<and> r < n"
1.16    proof (induct m)
1.17      case 0 with \<open>n \<noteq> 0\<close>
1.18 -    have "(0\<Colon>nat) = 0 * n + 0 \<and> 0 < n" by simp
1.19 +    have "(0::nat) = 0 * n + 0 \<and> 0 < n" by simp
1.20      then show ?case by blast
1.21    next
1.22      case (Suc m) then obtain q' r'
1.23 @@ -868,7 +868,7 @@
1.25  next
1.26    case False
1.27 -  have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q\<Colon>nat)"
1.28 +  have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q::nat)"
1.29    apply (rule leI)
1.32 @@ -1115,10 +1115,10 @@
1.33    then show "m div n * n + m mod n \<le> m" by auto
1.34  qed
1.35
1.36 -lemma mod_geq: "\<not> m < (n\<Colon>nat) \<Longrightarrow> m mod n = (m - n) mod n"
1.37 +lemma mod_geq: "\<not> m < (n::nat) \<Longrightarrow> m mod n = (m - n) mod n"
1.38  by (simp add: le_mod_geq linorder_not_less)
1.39
1.40 -lemma mod_if: "m mod (n\<Colon>nat) = (if m < n then m else (m - n) mod n)"
1.41 +lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
1.43
1.44  lemma mod_1 [simp]: "m mod Suc 0 = 0"
1.45 @@ -1313,7 +1313,7 @@
1.46
1.47  lemma split_div_lemma:
1.48    assumes "0 < n"
1.49 -  shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m\<Colon>nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
1.50 +  shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m::nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
1.51  proof
1.52    assume ?rhs
1.53    with mult_div_cancel have nq: "n * q = m - (m mod n)" by simp
1.54 @@ -1486,7 +1486,7 @@
1.55  lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
1.56  by (simp add: mult_2 [symmetric])
1.57
1.58 -lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
1.59 +lemma mod2_gr_0 [simp]: "0 < (m::nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
1.60  proof -
1.61    { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
1.62    moreover have "m mod 2 < 2" by simp
1.63 @@ -1999,7 +1999,7 @@
1.64  lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
1.65
1.66  lemma zmod_zdiv_equality' [nitpick_unfold]:
1.67 -  "(m\<Colon>int) mod n = m - (m div n) * n"
1.68 +  "(m::int) mod n = m - (m div n) * n"
1.69    using mod_div_equality [of m n] by arith
1.70
1.71
```