src/HOL/Nat.thy
changeset 27104 791607529f6d
parent 26748 4d51ddd6aa5c
child 27129 336807f865ce
     1.1 --- a/src/HOL/Nat.thy	Tue Jun 10 15:30:06 2008 +0200
     1.2 +++ b/src/HOL/Nat.thy	Tue Jun 10 15:30:33 2008 +0200
     1.3 @@ -43,12 +43,12 @@
     1.4  global
     1.5  
     1.6  typedef (open Nat)
     1.7 -  nat = "Collect Nat"
     1.8 -  by (rule exI, rule CollectI, rule Nat.Zero_RepI)
     1.9 +  nat = Nat
    1.10 +  by (rule exI, unfold mem_def, rule Nat.Zero_RepI)
    1.11  
    1.12  constdefs
    1.13 -  Suc :: "nat => nat"
    1.14 -  Suc_def:      "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
    1.15 +  Suc ::   "nat => nat"
    1.16 +  Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
    1.17  
    1.18  local
    1.19  
    1.20 @@ -62,34 +62,32 @@
    1.21  
    1.22  end
    1.23  
    1.24 -lemma nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n"
    1.25 -  apply (unfold Zero_nat_def Suc_def)
    1.26 -  apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
    1.27 -  apply (erule Rep_Nat [THEN CollectD, THEN Nat.induct])
    1.28 -  apply (iprover elim: Abs_Nat_inverse [OF CollectI, THEN subst])
    1.29 -  done
    1.30 +lemma Suc_not_Zero: "Suc m \<noteq> 0"
    1.31 +apply (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def] Rep_Nat [unfolded mem_def] Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def]) 
    1.32 +done
    1.33  
    1.34 -lemma Suc_not_Zero [iff]: "Suc m \<noteq> 0"
    1.35 -  by (simp add: Zero_nat_def Suc_def
    1.36 -    Abs_Nat_inject Rep_Nat [THEN CollectD] Suc_RepI Zero_RepI
    1.37 -      Suc_Rep_not_Zero_Rep)
    1.38 -
    1.39 -lemma Zero_not_Suc [iff]: "0 \<noteq> Suc m"
    1.40 +lemma Zero_not_Suc: "0 \<noteq> Suc m"
    1.41    by (rule not_sym, rule Suc_not_Zero not_sym)
    1.42  
    1.43 -lemma inj_Suc[simp]: "inj_on Suc N"
    1.44 -  by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat [THEN CollectD] Suc_RepI
    1.45 -                inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject)
    1.46 -
    1.47 -lemma Suc_Suc_eq [iff]: "Suc m = Suc n \<longleftrightarrow> m = n"
    1.48 -  by (rule inj_Suc [THEN inj_eq])
    1.49 +rep_datatype "0 \<Colon> nat" Suc
    1.50 +apply (unfold Zero_nat_def Suc_def)
    1.51 +apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
    1.52 +apply (erule Rep_Nat [unfolded mem_def, THEN Nat.induct])
    1.53 +apply (iprover elim: Abs_Nat_inverse [unfolded mem_def, THEN subst])
    1.54 +apply (simp_all add: Abs_Nat_inject [unfolded mem_def] Rep_Nat [unfolded mem_def]
    1.55 +  Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def]
    1.56 +  Suc_Rep_not_Zero_Rep [unfolded mem_def, symmetric]
    1.57 +  inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject)
    1.58 +done
    1.59  
    1.60 -rep_datatype nat
    1.61 -  distinct  Suc_not_Zero Zero_not_Suc
    1.62 -  inject    Suc_Suc_eq
    1.63 -  induction nat_induct
    1.64 +lemma nat_induct [case_names 0 Suc, induct type: nat]:
    1.65 +  -- {* for backward compatibility -- naming of variables differs *}
    1.66 +  fixes n
    1.67 +  assumes "P 0"
    1.68 +    and "\<And>n. P n \<Longrightarrow> P (Suc n)"
    1.69 +  shows "P n"
    1.70 +  using assms by (rule nat.induct) 
    1.71  
    1.72 -declare nat.induct [case_names 0 Suc, induct type: nat]
    1.73  declare nat.exhaust [case_names 0 Suc, cases type: nat]
    1.74  
    1.75  lemmas nat_rec_0 = nat.recs(1)
    1.76 @@ -97,10 +95,13 @@
    1.77  
    1.78  lemmas nat_case_0 = nat.cases(1)
    1.79    and nat_case_Suc = nat.cases(2)
    1.80 -
    1.81 +   
    1.82  
    1.83  text {* Injectiveness and distinctness lemmas *}
    1.84  
    1.85 +lemma inj_Suc[simp]: "inj_on Suc N"
    1.86 +  by (simp add: inj_on_def)
    1.87 +
    1.88  lemma Suc_neq_Zero: "Suc m = 0 \<Longrightarrow> R"
    1.89  by (rule notE, rule Suc_not_Zero)
    1.90  
    1.91 @@ -1245,7 +1246,7 @@
    1.92  
    1.93  definition
    1.94    Nats  :: "'a set" where
    1.95 -  "Nats = range of_nat"
    1.96 +  [code func del]: "Nats = range of_nat"
    1.97  
    1.98  notation (xsymbols)
    1.99    Nats  ("\<nat>")