src/HOL/Nat.thy
changeset 27129 336807f865ce
parent 27104 791607529f6d
child 27213 2c7a628ccdcf
     1.1 --- a/src/HOL/Nat.thy	Tue Jun 10 19:15:21 2008 +0200
     1.2 +++ b/src/HOL/Nat.thy	Tue Jun 10 19:15:21 2008 +0200
     1.3 @@ -63,22 +63,23 @@
     1.4  end
     1.5  
     1.6  lemma Suc_not_Zero: "Suc m \<noteq> 0"
     1.7 -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.8 -done
     1.9 +  apply (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def]
    1.10 +    Rep_Nat [unfolded mem_def] Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def])
    1.11 +  done
    1.12  
    1.13  lemma Zero_not_Suc: "0 \<noteq> Suc m"
    1.14    by (rule not_sym, rule Suc_not_Zero not_sym)
    1.15  
    1.16  rep_datatype "0 \<Colon> nat" Suc
    1.17 -apply (unfold Zero_nat_def Suc_def)
    1.18 -apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
    1.19 -apply (erule Rep_Nat [unfolded mem_def, THEN Nat.induct])
    1.20 -apply (iprover elim: Abs_Nat_inverse [unfolded mem_def, THEN subst])
    1.21 -apply (simp_all add: Abs_Nat_inject [unfolded mem_def] Rep_Nat [unfolded mem_def]
    1.22 -  Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def]
    1.23 -  Suc_Rep_not_Zero_Rep [unfolded mem_def, symmetric]
    1.24 -  inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject)
    1.25 -done
    1.26 +  apply (unfold Zero_nat_def Suc_def)
    1.27 +     apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
    1.28 +     apply (erule Rep_Nat [unfolded mem_def, THEN Nat.induct])
    1.29 +     apply (iprover elim: Abs_Nat_inverse [unfolded mem_def, THEN subst])
    1.30 +    apply (simp_all add: Abs_Nat_inject [unfolded mem_def] Rep_Nat [unfolded mem_def]
    1.31 +      Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def]
    1.32 +      Suc_Rep_not_Zero_Rep [unfolded mem_def, symmetric]
    1.33 +      inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject)
    1.34 +  done
    1.35  
    1.36  lemma nat_induct [case_names 0 Suc, induct type: nat]:
    1.37    -- {* for backward compatibility -- naming of variables differs *}
    1.38 @@ -88,6 +89,10 @@
    1.39    shows "P n"
    1.40    using assms by (rule nat.induct) 
    1.41  
    1.42 +ML {*
    1.43 +  fun nat_induct_tac n = res_inst_tac [("n", n)] @{thm nat_induct}
    1.44 +*}
    1.45 +
    1.46  declare nat.exhaust [case_names 0 Suc, cases type: nat]
    1.47  
    1.48  lemmas nat_rec_0 = nat.recs(1)