src/HOL/Nat.thy
changeset 34208 a7acd6c68d9b
parent 33657 a4179bf442d1
child 35028 108662d50512
     1.1 --- a/src/HOL/Nat.thy	Tue Dec 29 20:59:47 2009 +0100
     1.2 +++ b/src/HOL/Nat.thy	Wed Dec 30 01:08:33 2009 +0100
     1.3 @@ -27,10 +27,9 @@
     1.4    Suc_Rep :: "ind => ind"
     1.5  where
     1.6    -- {* the axiom of infinity in 2 parts *}
     1.7 -  inj_Suc_Rep:          "inj Suc_Rep" and
     1.8 +  Suc_Rep_inject:       "Suc_Rep x = Suc_Rep y ==> x = y" and
     1.9    Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
    1.10  
    1.11 -
    1.12  subsection {* Type nat *}
    1.13  
    1.14  text {* Type definition *}
    1.15 @@ -69,6 +68,9 @@
    1.16  lemma Zero_not_Suc: "0 \<noteq> Suc m"
    1.17    by (rule not_sym, rule Suc_not_Zero not_sym)
    1.18  
    1.19 +lemma Suc_Rep_inject': "Suc_Rep x = Suc_Rep y \<longleftrightarrow> x = y"
    1.20 +  by (rule iffI, rule Suc_Rep_inject) simp_all
    1.21 +
    1.22  rep_datatype "0 \<Colon> nat" Suc
    1.23    apply (unfold Zero_nat_def Suc_def)
    1.24       apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
    1.25 @@ -77,7 +79,7 @@
    1.26      apply (simp_all add: Abs_Nat_inject [unfolded mem_def] Rep_Nat [unfolded mem_def]
    1.27        Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def]
    1.28        Suc_Rep_not_Zero_Rep [unfolded mem_def, symmetric]
    1.29 -      inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject)
    1.30 +      Suc_Rep_inject' Rep_Nat_inject)
    1.31    done
    1.32  
    1.33  lemma nat_induct [case_names 0 Suc, induct type: nat]: