src/HOL/Library/Extended_Nat.thy
changeset 61076 bdc1e2f0a86a
parent 60679 ade12ef2773c
child 61378 3e04c9ca001a
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Tue Sep 01 17:25:36 2015 +0200
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Sep 01 22:32:58 2015 +0200
     1.3 @@ -112,8 +112,8 @@
     1.4    by (simp add: zero_enat_def)
     1.5  
     1.6  lemma zero_one_enat_neq [simp]:
     1.7 -  "\<not> 0 = (1\<Colon>enat)"
     1.8 -  "\<not> 1 = (0\<Colon>enat)"
     1.9 +  "\<not> 0 = (1::enat)"
    1.10 +  "\<not> 1 = (0::enat)"
    1.11    unfolding zero_enat_def one_enat_def by simp_all
    1.12  
    1.13  lemma infinity_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1"
    1.14 @@ -380,14 +380,14 @@
    1.15  a generalize linordered_semidom to a new class that includes enat? *)
    1.16  
    1.17  lemma enat_ord_number [simp]:
    1.18 -  "(numeral m \<Colon> enat) \<le> numeral n \<longleftrightarrow> (numeral m \<Colon> nat) \<le> numeral n"
    1.19 -  "(numeral m \<Colon> enat) < numeral n \<longleftrightarrow> (numeral m \<Colon> nat) < numeral n"
    1.20 +  "(numeral m :: enat) \<le> numeral n \<longleftrightarrow> (numeral m :: nat) \<le> numeral n"
    1.21 +  "(numeral m :: enat) < numeral n \<longleftrightarrow> (numeral m :: nat) < numeral n"
    1.22    by (simp_all add: numeral_eq_enat)
    1.23  
    1.24 -lemma i0_lb [simp]: "(0\<Colon>enat) \<le> n"
    1.25 +lemma i0_lb [simp]: "(0::enat) \<le> n"
    1.26    by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
    1.27  
    1.28 -lemma ile0_eq [simp]: "n \<le> (0\<Colon>enat) \<longleftrightarrow> n = 0"
    1.29 +lemma ile0_eq [simp]: "n \<le> (0::enat) \<longleftrightarrow> n = 0"
    1.30    by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
    1.31  
    1.32  lemma infinity_ileE [elim!]: "\<infinity> \<le> enat m \<Longrightarrow> R"
    1.33 @@ -396,10 +396,10 @@
    1.34  lemma infinity_ilessE [elim!]: "\<infinity> < enat m \<Longrightarrow> R"
    1.35    by simp
    1.36  
    1.37 -lemma not_iless0 [simp]: "\<not> n < (0\<Colon>enat)"
    1.38 +lemma not_iless0 [simp]: "\<not> n < (0::enat)"
    1.39    by (simp add: zero_enat_def less_enat_def split: enat.splits)
    1.40  
    1.41 -lemma i0_less [simp]: "(0\<Colon>enat) < n \<longleftrightarrow> n \<noteq> 0"
    1.42 +lemma i0_less [simp]: "(0::enat) < n \<longleftrightarrow> n \<noteq> 0"
    1.43    by (simp add: zero_enat_def less_enat_def split: enat.splits)
    1.44  
    1.45  lemma eSuc_ile_mono [simp]: "eSuc n \<le> eSuc m \<longleftrightarrow> n \<le> m"
    1.46 @@ -623,7 +623,7 @@
    1.47  instance enat :: wellorder
    1.48  proof
    1.49    fix P and n
    1.50 -  assume hyp: "(\<And>n\<Colon>enat. (\<And>m\<Colon>enat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
    1.51 +  assume hyp: "(\<And>n::enat. (\<And>m::enat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
    1.52    show "P n" by (blast intro: enat_less_induct hyp)
    1.53  qed
    1.54