src/HOL/Nat.thy
changeset 61076 bdc1e2f0a86a
parent 61070 b72a990adfe2
child 61144 5e94dfead1c2
     1.1 --- a/src/HOL/Nat.thy	Tue Sep 01 17:25:36 2015 +0200
     1.2 +++ b/src/HOL/Nat.thy	Tue Sep 01 22:32:58 2015 +0200
     1.3 @@ -85,10 +85,10 @@
     1.4  done
     1.5  
     1.6  free_constructors case_nat for
     1.7 -    "0 \<Colon> nat"
     1.8 +    "0 :: nat"
     1.9    | Suc pred
    1.10  where
    1.11 -  "pred (0 \<Colon> nat) = (0 \<Colon> nat)"
    1.12 +  "pred (0 :: nat) = (0 :: nat)"
    1.13      apply atomize_elim
    1.14      apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
    1.15     apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI Suc_Rep_inject'
    1.16 @@ -99,7 +99,7 @@
    1.17  -- \<open>Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}.\<close>
    1.18  setup \<open>Sign.mandatory_path "old"\<close>
    1.19  
    1.20 -old_rep_datatype "0 \<Colon> nat" Suc
    1.21 +old_rep_datatype "0 :: nat" Suc
    1.22    apply (erule nat_induct0, assumption)
    1.23   apply (rule nat.inject)
    1.24  apply (rule nat.distinct(1))
    1.25 @@ -216,7 +216,7 @@
    1.26  begin
    1.27  
    1.28  primrec plus_nat where
    1.29 -  add_0:      "0 + n = (n\<Colon>nat)"
    1.30 +  add_0:      "0 + n = (n::nat)"
    1.31  | add_Suc:  "Suc m + n = Suc (m + n)"
    1.32  
    1.33  lemma add_0_right [simp]: "m + 0 = (m::nat)"
    1.34 @@ -231,7 +231,7 @@
    1.35    by simp
    1.36  
    1.37  primrec minus_nat where
    1.38 -  diff_0 [code]: "m - 0 = (m\<Colon>nat)"
    1.39 +  diff_0 [code]: "m - 0 = (m::nat)"
    1.40  | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
    1.41  
    1.42  declare diff_Suc [simp del]
    1.43 @@ -263,7 +263,7 @@
    1.44    One_nat_def [simp]: "1 = Suc 0"
    1.45  
    1.46  primrec times_nat where
    1.47 -  mult_0:     "0 * n = (0\<Colon>nat)"
    1.48 +  mult_0: "0 * n = (0::nat)"
    1.49  | mult_Suc: "Suc m * n = n + (m * n)"
    1.50  
    1.51  lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
    1.52 @@ -349,7 +349,7 @@
    1.53  
    1.54  subsubsection \<open>Difference\<close>
    1.55  
    1.56 -lemma diff_self_eq_0 [simp]: "(m\<Colon>nat) - m = 0"
    1.57 +lemma diff_self_eq_0 [simp]: "(m::nat) - m = 0"
    1.58    by (fact diff_cancel)
    1.59  
    1.60  lemma diff_diff_left: "(i::nat) - j - k = i - (j + k)"
    1.61 @@ -435,12 +435,12 @@
    1.62  begin
    1.63  
    1.64  primrec less_eq_nat where
    1.65 -  "(0\<Colon>nat) \<le> n \<longleftrightarrow> True"
    1.66 +  "(0::nat) \<le> n \<longleftrightarrow> True"
    1.67  | "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
    1.68  
    1.69  declare less_eq_nat.simps [simp del]
    1.70 -lemma le0 [iff]: "0 \<le> (n\<Colon>nat)" by (simp add: less_eq_nat.simps)
    1.71 -lemma [code]: "(0\<Colon>nat) \<le> n \<longleftrightarrow> True" by simp
    1.72 +lemma le0 [iff]: "0 \<le> (n::nat)" by (simp add: less_eq_nat.simps)
    1.73 +lemma [code]: "(0::nat) \<le> n \<longleftrightarrow> True" by simp
    1.74  
    1.75  definition less_nat where
    1.76    less_eq_Suc_le: "n < m \<longleftrightarrow> Suc n \<le> m"
    1.77 @@ -451,13 +451,13 @@
    1.78  lemma Suc_le_eq [code]: "Suc m \<le> n \<longleftrightarrow> m < n"
    1.79    unfolding less_eq_Suc_le ..
    1.80  
    1.81 -lemma le_0_eq [iff]: "(n\<Colon>nat) \<le> 0 \<longleftrightarrow> n = 0"
    1.82 +lemma le_0_eq [iff]: "(n::nat) \<le> 0 \<longleftrightarrow> n = 0"
    1.83    by (induct n) (simp_all add: less_eq_nat.simps(2))
    1.84  
    1.85 -lemma not_less0 [iff]: "\<not> n < (0\<Colon>nat)"
    1.86 +lemma not_less0 [iff]: "\<not> n < (0::nat)"
    1.87    by (simp add: less_eq_Suc_le)
    1.88  
    1.89 -lemma less_nat_zero_code [code]: "n < (0\<Colon>nat) \<longleftrightarrow> False"
    1.90 +lemma less_nat_zero_code [code]: "n < (0::nat) \<longleftrightarrow> False"
    1.91    by simp
    1.92  
    1.93  lemma Suc_less_eq [iff]: "Suc m < Suc n \<longleftrightarrow> m < n"
    1.94 @@ -1290,10 +1290,10 @@
    1.95  begin
    1.96  
    1.97  definition
    1.98 -  "(inf \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = min"
    1.99 +  "(inf :: nat \<Rightarrow> nat \<Rightarrow> nat) = min"
   1.100  
   1.101  definition
   1.102 -  "(sup \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = max"
   1.103 +  "(sup :: nat \<Rightarrow> nat \<Rightarrow> nat) = max"
   1.104  
   1.105  instance by intro_classes
   1.106    (auto simp add: inf_nat_def sup_nat_def max_def not_le min_def
   1.107 @@ -1934,7 +1934,7 @@
   1.108  
   1.109  text \<open>@{term "op dvd"} is a partial order\<close>
   1.110  
   1.111 -interpretation dvd: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
   1.112 +interpretation dvd: order "op dvd" "\<lambda>n m :: nat. n dvd m \<and> \<not> m dvd n"
   1.113    proof qed (auto intro: dvd_refl dvd_trans dvd_antisym)
   1.114  
   1.115  lemma dvd_diff_nat[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
   1.116 @@ -2021,7 +2021,7 @@
   1.117  begin
   1.118  
   1.119  definition size_nat where
   1.120 -  [simp, code]: "size (n \<Colon> nat) = n"
   1.121 +  [simp, code]: "size (n::nat) = n"
   1.122  
   1.123  instance ..
   1.124