src/HOL/Code_Numeral.thy

   fixes m :: natural
   assumes "\<And>n. m = of_nat n \<Longrightarrow> P"
   shows P
   using assms by transfer blast
 
+instantiation natural :: size
+begin
+
+definition size_natural :: "natural \<Rightarrow> nat" where
+  [simp, code]: "size_natural = nat_of_natural"
+
+instance ..
+
+end
+
 lemma natural_decr [termination_simp]:
   "n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n"
   by transfer simp
 
-lemma natural_zero_minus_one:
-  "(0::natural) - 1 = 0"
-  by simp
-
-lemma Suc_natural_minus_one:
-  "Suc n - 1 = n"
+lemma natural_zero_minus_one: "(0::natural) - 1 = 0"
+  by (rule zero_diff)
+
+lemma Suc_natural_minus_one: "Suc n - 1 = n"
   by transfer simp
 
 hide_const (open) Suc
 
 

 
 lemma [code]:
   "HOL.equal m n \<longleftrightarrow> HOL.equal (integer_of_natural m) (integer_of_natural n)"
   by transfer (simp add: equal)
 
-lemma [code nbe]:
-  "HOL.equal n (n::natural) \<longleftrightarrow> True"
-  by (simp add: equal)
-
-lemma [code]:
-  "m \<le> n \<longleftrightarrow> integer_of_natural m \<le> integer_of_natural n"
-  by transfer simp
-
-lemma [code]:
-  "m < n \<longleftrightarrow> integer_of_natural m < integer_of_natural n"
+lemma [code nbe]: "HOL.equal n (n::natural) \<longleftrightarrow> True"
+  by (rule equal_class.equal_refl)
+
+lemma [code]: "m \<le> n \<longleftrightarrow> integer_of_natural m \<le> integer_of_natural n"
+  by transfer simp
+
+lemma [code]: "m < n \<longleftrightarrow> integer_of_natural m < integer_of_natural n"
   by transfer simp
 
 hide_const (open) Nat
 
 lifting_update integer.lifting

 code_reflect Code_Numeral
   datatypes natural = _
   functions integer_of_natural natural_of_integer
 
 end
-