src/HOL/Nat.thy
changeset 24162 8dfd5dd65d82
parent 24091 109f19a13872
child 24196 f1dbfd7e3223
     1.1 --- a/src/HOL/Nat.thy	Tue Aug 07 09:38:43 2007 +0200
     1.2 +++ b/src/HOL/Nat.thy	Tue Aug 07 09:38:44 2007 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4    less_def: "m < n == (m, n) : pred_nat^+"
     1.5    le_def:   "m \<le> (n::nat) == ~ (n < m)" ..
     1.6  
     1.7 -lemmas [code func del] = less_def le_def
     1.8 +lemmas [code func del] = Zero_nat_def One_nat_def less_def le_def
     1.9  
    1.10  text {* Induction *}
    1.11  
    1.12 @@ -114,7 +114,24 @@
    1.13  class size = type +
    1.14    fixes size :: "'a \<Rightarrow> nat"
    1.15  
    1.16 -text {* @{typ nat} is a datatype *}
    1.17 +text {* now we are ready to re-invent primitive types
    1.18 +  -- dependency on class size is hardwired into datatype package *}
    1.19 +
    1.20 +rep_datatype bool
    1.21 +  distinct True_not_False False_not_True
    1.22 +  induction bool_induct
    1.23 +
    1.24 +rep_datatype unit
    1.25 +  induction unit_induct
    1.26 +
    1.27 +rep_datatype prod
    1.28 +  inject Pair_eq
    1.29 +  induction prod_induct
    1.30 +
    1.31 +rep_datatype sum
    1.32 +  distinct Inl_not_Inr Inr_not_Inl
    1.33 +  inject Inl_eq Inr_eq
    1.34 +  induction sum_induct
    1.35  
    1.36  rep_datatype nat
    1.37    distinct  Suc_not_Zero Zero_not_Suc
    1.38 @@ -130,7 +147,6 @@
    1.39  lemmas nat_case_0 = nat.cases(1)
    1.40    and nat_case_Suc = nat.cases(2)
    1.41  
    1.42 -
    1.43  lemma n_not_Suc_n: "n \<noteq> Suc n"
    1.44    by (induct n) simp_all
    1.45