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.24        (simp add: divmod_nat_rel_def)
    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.30    apply (subst less_iff_Suc_add)
    1.31    apply (auto simp add: add_mult_distrib)
    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.42  by (simp add: le_mod_geq)
    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