src/HOL/Nat.thy

 
 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
   by (fact Let_def)
 
 
-subsubsection {* Monotonicity of Multiplication *}
+subsubsection {* Monotonicity of multiplication *}
 
 lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k"
 by (simp add: mult_right_mono)
 
 lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j"

   show "(f^^k) bot \<le> lfp f"
     using Kleene_iter_lpfp[OF assms(1)] lfp_unfold[OF assms(1)] by simp
 qed
 
 
-subsection {* Embedding of the Naturals into any @{text semiring_1}: @{term of_nat} *}
+subsection {* Embedding of the naturals into any @{text semiring_1}: @{term of_nat} *}
 
 context semiring_1
 begin
 
 definition of_nat :: "nat \<Rightarrow> 'a" where

 
 lemma of_nat_eq_id [simp]: "of_nat = id"
   by (auto simp add: fun_eq_iff)
 
 
-subsection {* The Set of Natural Numbers *}
+subsection {* The set of natural numbers *}
 
 context semiring_1
 begin
 
 definition Nats  :: "'a set" where

   by (rule Nats_cases) auto
 
 end
 
 
-subsection {* Further Arithmetic Facts Concerning the Natural Numbers *}
+subsection {* Further arithmetic facts concerning the natural numbers *}
 
 lemma subst_equals:
   assumes 1: "t = s" and 2: "u = t"
   shows "u = s"
   using 2 1 by (rule trans)

 
 lemma dec_induct[consumes 1, case_names base step]:
   "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j"
   by (induct j arbitrary: i) (auto simp: le_Suc_eq)
  
+
 subsection {* The divides relation on @{typ nat} *}
 
 lemma dvd_1_left [iff]: "Suc 0 dvd k"
 unfolding dvd_def by simp
 

   also have "\<dots> \<longleftrightarrow> m dvd n + (r * m - q)" by (simp add: add.commute)
   finally show ?thesis .
 qed
 
 
-subsection {* aliases *}
+subsection {* Aliases *}
 
 lemma nat_mult_1: "(1::nat) * n = n"
   by (rule mult_1_left)
  
 lemma nat_mult_1_right: "n * (1::nat) = n"
   by (rule mult_1_right)
 
 
-subsection {* size of a datatype value *}
+subsection {* Size of a datatype value *}
 
 class size =
   fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded} *}
 
-
-subsection {* code module namespace *}
+instantiation nat :: size
+begin
+
+definition size_nat where
+  [simp, code]: "size (n \<Colon> nat) = n"
+
+instance ..
+
+end
+
+
+subsection {* Code module namespace *}
 
 code_identifier
   code_module Nat \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 hide_const (open) of_nat_aux