src/HOL/Nat.thy
changeset 44278 1220ecb81e8f
parent 43595 7ae4a23b5be6
child 44325 84696670feb1
     1.1 --- a/src/HOL/Nat.thy	Thu Aug 18 13:25:17 2011 +0200
     1.2 +++ b/src/HOL/Nat.thy	Thu Aug 18 13:55:26 2011 +0200
     1.3 @@ -39,11 +39,20 @@
     1.4      Zero_RepI: "Nat Zero_Rep"
     1.5    | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
     1.6  
     1.7 -typedef (open Nat) nat = Nat
     1.8 -  by (rule exI, unfold mem_def, rule Nat.Zero_RepI)
     1.9 +typedef (open Nat) nat = "{n. Nat n}"
    1.10 +  using Nat.Zero_RepI by auto
    1.11 +
    1.12 +lemma Nat_Rep_Nat:
    1.13 +  "Nat (Rep_Nat n)"
    1.14 +  using Rep_Nat by simp
    1.15  
    1.16 -definition Suc :: "nat => nat" where
    1.17 -  "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
    1.18 +lemma Nat_Abs_Nat_inverse:
    1.19 +  "Nat n \<Longrightarrow> Rep_Nat (Abs_Nat n) = n"
    1.20 +  using Abs_Nat_inverse by simp
    1.21 +
    1.22 +lemma Nat_Abs_Nat_inject:
    1.23 +  "Nat n \<Longrightarrow> Nat m \<Longrightarrow> Abs_Nat n = Abs_Nat m \<longleftrightarrow> n = m"
    1.24 +  using Abs_Nat_inject by simp
    1.25  
    1.26  instantiation nat :: zero
    1.27  begin
    1.28 @@ -55,9 +64,11 @@
    1.29  
    1.30  end
    1.31  
    1.32 +definition Suc :: "nat \<Rightarrow> nat" where
    1.33 +  "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
    1.34 +
    1.35  lemma Suc_not_Zero: "Suc m \<noteq> 0"
    1.36 -  by (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def]
    1.37 -    Rep_Nat [unfolded mem_def] Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def])
    1.38 +  by (simp add: Zero_nat_def Suc_def Suc_RepI Zero_RepI Nat_Abs_Nat_inject Suc_Rep_not_Zero_Rep Nat_Rep_Nat)
    1.39  
    1.40  lemma Zero_not_Suc: "0 \<noteq> Suc m"
    1.41    by (rule not_sym, rule Suc_not_Zero not_sym)
    1.42 @@ -67,12 +78,12 @@
    1.43  
    1.44  rep_datatype "0 \<Colon> nat" Suc
    1.45    apply (unfold Zero_nat_def Suc_def)
    1.46 -     apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
    1.47 -     apply (erule Rep_Nat [unfolded mem_def, THEN Nat.induct])
    1.48 -     apply (iprover elim: Abs_Nat_inverse [unfolded mem_def, THEN subst])
    1.49 -    apply (simp_all add: Abs_Nat_inject [unfolded mem_def] Rep_Nat [unfolded mem_def]
    1.50 -      Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def]
    1.51 -      Suc_Rep_not_Zero_Rep [unfolded mem_def, symmetric]
    1.52 +  apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
    1.53 +   apply (erule Nat_Rep_Nat [THEN Nat.induct])
    1.54 +   apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
    1.55 +    apply (simp_all add: Nat_Abs_Nat_inject Nat_Rep_Nat
    1.56 +      Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep
    1.57 +      Suc_Rep_not_Zero_Rep [symmetric]
    1.58        Suc_Rep_inject' Rep_Nat_inject)
    1.59    done
    1.60