src/HOL/Nat.thy

   nat = Nat
 proof
   show "Zero_Rep : Nat" by (rule Nat.Zero_RepI)
 qed
 
-instance nat :: "{ord, zero, one}" ..
-
-
 text {* Abstract constants and syntax *}
 
 consts
   Suc :: "nat => nat"
   pred_nat :: "(nat * nat) set"
 
 local
 
 defs
+  Suc_def:      "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
+  pred_nat_def: "pred_nat == {(m, n). n = Suc m}"
+
+instance nat :: "{ord, zero, one}"
   Zero_nat_def: "0 == Abs_Nat Zero_Rep"
-  Suc_def:      "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
-  One_nat_def:  "1 == Suc 0"
-
-  -- {* nat operations *}
-  pred_nat_def: "pred_nat == {(m, n). n = Suc m}"
-
+  One_nat_def [simp]: "1 == Suc 0"
   less_def: "m < n == (m, n) : trancl pred_nat"
-
-  le_def: "m \<le> (n::nat) == ~ (n < m)"
-
-declare One_nat_def [simp]
-
+  le_def: "m \<le> (n::nat) == ~ (n < m)" ..
 
 text {* Induction *}
 
 theorem nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n"
   apply (unfold Zero_nat_def Suc_def)

 class power =
   fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"            (infixr "\<^loc>^" 80)
 
 text {* arithmetic operators @{text "+ -"} and @{text "*"} *}
 
-instance nat :: "{plus, minus, times, power}" ..
+instance nat :: "{plus, minus, times}" ..
 
 primrec
   add_0:    "0 + n = n"
   add_Suc:  "Suc m + n = Suc (m + n)"
 

   by simp
 
 instance nat :: eq ..
 
 lemma [code func]:
-  "Code_Generator.eq (0\<Colon>nat) 0 = True" unfolding eq_def by auto
+  "(0\<Colon>nat) = 0 \<longleftrightarrow> True" by auto
 
 lemma [code func]:
-  "Code_Generator.eq (Suc n) (Suc m) = Code_Generator.eq n m" unfolding eq_def by auto
+  "Suc n = Suc m \<longleftrightarrow> n = m" by auto
 
 lemma [code func]:
-  "Code_Generator.eq (Suc n) 0 = False" unfolding eq_def by auto
+  "Suc n = 0 \<longleftrightarrow> False" by auto
 
 lemma [code func]:
-  "Code_Generator.eq 0 (Suc m) = False" unfolding eq_def by auto
+  "0 = Suc m \<longleftrightarrow> False" by auto
 
 
 subsection {* Further Arithmetic Facts Concerning the Natural Numbers *}
 
 use "arith_data.ML"